Metamath Proof Explorer

Theorem lmod0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( ax-hvmul0 analog.) (Contributed by NM, 12-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypotheses lmod0vs.v ⊢ V = Base W
lmod0vs.f ⊢ F = Scalar ⁡ W
lmod0vs.s ⊢ · ˙ = ⋅ W
lmod0vs.o ⊢ O = 0 F
lmod0vs.z ⊢ 0 ˙ = 0 W
Assertion lmod0vs ⊢ W ∈ LMod ∧ X ∈ V → O · ˙ X = 0 ˙

Proof

Step Hyp Ref Expression
1 lmod0vs.v ⊢ V = Base W
2 lmod0vs.f ⊢ F = Scalar ⁡ W
3 lmod0vs.s ⊢ · ˙ = ⋅ W
4 lmod0vs.o ⊢ O = 0 F
5 lmod0vs.z ⊢ 0 ˙ = 0 W
6 simpl ⊢ W ∈ LMod ∧ X ∈ V → W ∈ LMod
7 2 lmodring ⊢ W ∈ LMod → F ∈ Ring
8 7 adantr ⊢ W ∈ LMod ∧ X ∈ V → F ∈ Ring
9 eqid ⊢ Base F = Base F
10 9 4 ring0cl ⊢ F ∈ Ring → O ∈ Base F
11 8 10 syl ⊢ W ∈ LMod ∧ X ∈ V → O ∈ Base F
12 simpr ⊢ W ∈ LMod ∧ X ∈ V → X ∈ V
13 eqid ⊢ + W = + W
14 eqid ⊢ + F = + F
15 1 13 2 3 9 14 lmodvsdir ⊢ W ∈ LMod ∧ O ∈ Base F ∧ O ∈ Base F ∧ X ∈ V → O + F O · ˙ X = O · ˙ X + W O · ˙ X
16 6 11 11 12 15 syl13anc ⊢ W ∈ LMod ∧ X ∈ V → O + F O · ˙ X = O · ˙ X + W O · ˙ X
17 ringgrp ⊢ F ∈ Ring → F ∈ Grp
18 8 17 syl ⊢ W ∈ LMod ∧ X ∈ V → F ∈ Grp
19 9 14 4 grplid ⊢ F ∈ Grp ∧ O ∈ Base F → O + F O = O
20 18 11 19 syl2anc ⊢ W ∈ LMod ∧ X ∈ V → O + F O = O
21 20 oveq1d ⊢ W ∈ LMod ∧ X ∈ V → O + F O · ˙ X = O · ˙ X
22 16 21 eqtr3d ⊢ W ∈ LMod ∧ X ∈ V → O · ˙ X + W O · ˙ X = O · ˙ X
23 1 2 3 9 lmodvscl ⊢ W ∈ LMod ∧ O ∈ Base F ∧ X ∈ V → O · ˙ X ∈ V
24 6 11 12 23 syl3anc ⊢ W ∈ LMod ∧ X ∈ V → O · ˙ X ∈ V
25 1 13 5 lmod0vid ⊢ W ∈ LMod ∧ O · ˙ X ∈ V → O · ˙ X + W O · ˙ X = O · ˙ X ↔ 0 ˙ = O · ˙ X
26 24 25 syldan ⊢ W ∈ LMod ∧ X ∈ V → O · ˙ X + W O · ˙ X = O · ˙ X ↔ 0 ˙ = O · ˙ X
27 22 26 mpbid ⊢ W ∈ LMod ∧ X ∈ V → 0 ˙ = O · ˙ X
28 27 eqcomd ⊢ W ∈ LMod ∧ X ∈ V → O · ˙ X = 0 ˙