Metamath Proof Explorer

Theorem slmdvs0

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) (Revised by Thierry Arnoux, 1-Apr-2018)

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

Proof

Step Hyp Ref Expression
1 slmdvs0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 slmdvs0.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 slmdvs0.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
4 slmdvs0.z ⊢ 0 = ( 0g ‘ 𝑊 )
5 1 slmdsrg ⊢ ( 𝑊 ∈ SLMod → 𝐹 ∈ SRing )
6 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
7 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
8 3 6 7 srgrz ⊢ ( ( 𝐹 ∈ SRing ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝐹 ) )
9 5 8 sylan ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝐹 ) )
10 9 oveq1d ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( ( 0g ‘ 𝐹 ) · 0 ) )
11 simpl ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → 𝑊 ∈ SLMod )
12 simpr ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 )
13 5 adantr ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → 𝐹 ∈ SRing )
14 3 7 srg0cl ⊢ ( 𝐹 ∈ SRing → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
15 13 14 syl ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( 0g ‘ 𝐹 ) ∈ 𝐾 )
16 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
17 16 4 slmd0vcl ⊢ ( 𝑊 ∈ SLMod → 0 ∈ ( Base ‘ 𝑊 ) )
18 17 adantr ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → 0 ∈ ( Base ‘ 𝑊 ) )
19 16 1 2 3 6 slmdvsass ⊢ ( ( 𝑊 ∈ SLMod ∧ ( 𝑋 ∈ 𝐾 ∧ ( 0g ‘ 𝐹 ) ∈ 𝐾 ∧ 0 ∈ ( Base ‘ 𝑊 ) ) ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) )
20 11 12 15 18 19 syl13anc ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) )
21 16 1 2 7 4 slmd0vs ⊢ ( ( 𝑊 ∈ SLMod ∧ 0 ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝐹 ) · 0 ) = 0 )
22 18 21 syldan ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 0g ‘ 𝐹 ) · 0 ) = 0 )
23 22 oveq2d ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 · ( ( 0g ‘ 𝐹 ) · 0 ) ) = ( 𝑋 · 0 ) )
24 20 23 eqtrd ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑋 ( .r ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) · 0 ) = ( 𝑋 · 0 ) )
25 10 24 22 3eqtr3d ⊢ ( ( 𝑊 ∈ SLMod ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 · 0 ) = 0 )