Theorem clm0vs

Description: Zero times a vector is the zero vector. Equation 1a of Kreyszig p. 51. ( lmod0vs analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0vs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	clm0vs.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clm0vs.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	clm0vs.z	⊢ 0 = ( 0g ‘ 𝑊 )
Assertion	clm0vs	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 · 𝑋 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		clm0vs.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		clm0vs.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		clm0vs.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
4		clm0vs.z	⊢ 0 = ( 0g ‘ 𝑊 )
5	2	clm0	⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ 𝐹 ) )
6	5	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → 0 = ( 0g ‘ 𝐹 ) )
7	6	oveq1d	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 · 𝑋 ) = ( ( 0g ‘ 𝐹 ) · 𝑋 ) )
8		clmlmod	⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
9		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
10	1 2 3 9 4	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = 0 )
11	8 10	sylan	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = 0 )
12	7 11	eqtrd	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 · 𝑋 ) = 0 )