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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmod0vs.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmod0vs.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmod0vs.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
lmod0vs.z ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion lmod0vs ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑂 · 𝑋 ) = 0 )

Proof

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