Theorem lcd0vs

Description: A scalar zero times a functional is the zero functional. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcd0vs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcd0vs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcd0vs.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	lcd0vs.z	⊢ 0 = ( 0g ‘ 𝑅 )
	lcd0vs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcd0vs.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcd0vs.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
	lcd0vs.o	⊢ 𝑂 = ( 0g ‘ 𝐶 )
	lcd0vs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcd0vs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion	lcd0vs	⊢ ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		lcd0vs.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcd0vs.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		lcd0vs.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4		lcd0vs.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		lcd0vs.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		lcd0vs.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
7		lcd0vs.t	⊢ · = ( ·𝑠 ‘ 𝐶 )
8		lcd0vs.o	⊢ 𝑂 = ( 0g ‘ 𝐶 )
9		lcd0vs.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10		lcd0vs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
11		eqid	⊢ ( Scalar ‘ 𝐶 ) = ( Scalar ‘ 𝐶 )
12		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = ( 0g ‘ ( Scalar ‘ 𝐶 ) )
13	1 2 3 4 5 11 12 9	lcd0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐶 ) ) = 0 )
14	13	oveq1d	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = ( 0 · 𝐺 ) )
15	1 5 9	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
16	6 11 7 12 8	lmod0vs	⊢ ( ( 𝐶 ∈ LMod ∧ 𝐺 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝑂 )
17	15 10 16	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐶 ) ) · 𝐺 ) = 𝑂 )
18	14 17	eqtr3d	⊢ ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )