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

Metamath Proof Explorer

Theorem lmodvs0

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

Ref Expression
Hypotheses lmodvs0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvs0.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvs0.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lmodvs0.z ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion lmodvs0 ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 · 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 lmodvs0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 lmodvs0.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lmodvs0.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 lmodvs0.z ⊢ 0 = ( 0g ‘ 𝑊 )
5 1 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
6 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
7 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
8 3 6 7 ringrz ⊢ ( ( 𝐹 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝐹 ) )
9 5 8 sylan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝐹 ) )
10 9 oveq1d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( ( 0g ‘ 𝐹 ) · 0 ) )
11 simpl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → 𝑊 ∈ LMod )
12 simpr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
13 5 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → 𝐹 ∈ Ring )
14 3 7 ring0cl ⊢ ( 𝐹 ∈ Ring → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
15 13 14 syl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
16 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17 16 4 lmod0vcl ⊢ ( 𝑊 ∈ LMod → 0 ∈ ( Base ‘ 𝑊 ) )
18 17 adantr ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → 0 ∈ ( Base ‘ 𝑊 ) )
19 16 1 2 3 6 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 ∈ 𝐾 ∧ ( 0g ‘ 𝐹 ) ∈ 𝐾 ∧ 0 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) )
20 11 12 15 18 19 syl13anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) )
21 16 1 2 7 4 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 0 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝐹 ) · 0 ) = 0 )
22 18 21 syldan ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 0g ‘ 𝐹 ) · 0 ) = 0 )
23 22 oveq2d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) = ( 𝑋 · 0 ) )
24 20 23 eqtrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · 0 ) )
25 10 24 22 3eqtr3d ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 · 0 ) = 0 )