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 )