# 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 )