Theorem ldual0vs

Description: Scalar zero times a functional is the zero functional. (Contributed by NM, 17-Feb-2015)

	Ref	Expression
Hypotheses	ldual0vs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	ldual0vs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldual0vs.z	⊢ 0 = ( 0g ‘ 𝑅 )
	ldual0vs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldual0vs.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	ldual0vs.o	⊢ 𝑂 = ( 0g ‘ 𝐷 )
	ldual0vs.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldual0vs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	ldual0vs	⊢ ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		ldual0vs.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
2		ldual0vs.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
3		ldual0vs.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		ldual0vs.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		ldual0vs.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
6		ldual0vs.o	⊢ 𝑂 = ( 0g ‘ 𝐷 )
7		ldual0vs.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		ldual0vs.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
10		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = ( 0g ‘ ( Scalar ‘ 𝐷 ) )
11	2 3 4 9 10 7	ldual0	⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ 𝐷 ) ) = 0 )
12	11	oveq1d	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = ( 0 · 𝐺 ) )
13	4 7	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
14		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
15	1 4 14 7 8	ldualelvbase	⊢ ( 𝜑 → 𝐺 ∈ ( Base ‘ 𝐷 ) )
16	14 9 5 10 6	lmod0vs	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐺 ∈ ( Base ‘ 𝐷 ) ) → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = 𝑂 )
17	13 15 16	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝐷 ) ) · 𝐺 ) = 𝑂 )
18	12 17	eqtr3d	⊢ ( 𝜑 → ( 0 · 𝐺 ) = 𝑂 )