This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmodvscl

Description: Closure of scalar product for a left module. ( hvmulcl analog.) (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmodvscl.v ⊢ V = Base W
lmodvscl.f ⊢ F = Scalar ⁡ W
lmodvscl.s ⊢ · ˙ = ⋅ W
lmodvscl.k ⊢ K = Base F
Assertion lmodvscl ⊢ W ∈ LMod ∧ R ∈ K ∧ X ∈ V → R · ˙ X ∈ V

Proof

Step Hyp Ref Expression
1 lmodvscl.v ⊢ V = Base W
2 lmodvscl.f ⊢ F = Scalar ⁡ W
3 lmodvscl.s ⊢ · ˙ = ⋅ W
4 lmodvscl.k ⊢ K = Base F
5 biid ⊢ W ∈ LMod ↔ W ∈ LMod
6 pm4.24 ⊢ R ∈ K ↔ R ∈ K ∧ R ∈ K
7 pm4.24 ⊢ X ∈ V ↔ X ∈ V ∧ X ∈ V
8 eqid ⊢ + W = + W
9 eqid ⊢ + F = + F
10 eqid ⊢ ⋅ F = ⋅ F
11 eqid ⊢ 1 F = 1 F
12 1 8 3 2 4 9 10 11 lmodlema ⊢ W ∈ LMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V ∧ R · ˙ X + W X = R · ˙ X + W R · ˙ X ∧ R + F R · ˙ X = R · ˙ X + W R · ˙ X ∧ R ⋅ F R · ˙ X = R · ˙ R · ˙ X ∧ 1 F · ˙ X = X
13 12 simpld ⊢ W ∈ LMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V ∧ R · ˙ X + W X = R · ˙ X + W R · ˙ X ∧ R + F R · ˙ X = R · ˙ X + W R · ˙ X
14 13 simp1d ⊢ W ∈ LMod ∧ R ∈ K ∧ R ∈ K ∧ X ∈ V ∧ X ∈ V → R · ˙ X ∈ V
15 5 6 7 14 syl3anb ⊢ W ∈ LMod ∧ R ∈ K ∧ X ∈ V → R · ˙ X ∈ V