Theorem ldual0vs

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

	Ref	Expression
Hypotheses	ldual0vs.f	|- F = ( LFnl ` W )
	ldual0vs.r	|- R = ( Scalar ` W )
	ldual0vs.z	|- .0. = ( 0g ` R )
	ldual0vs.d	|- D = ( LDual ` W )
	ldual0vs.t	|- .x. = ( .s ` D )
	ldual0vs.o	|- O = ( 0g ` D )
	ldual0vs.w	|- ( ph -> W e. LMod )
	ldual0vs.g	|- ( ph -> G e. F )
Assertion	ldual0vs	|- ( ph -> ( .0. .x. G ) = O )

Proof

Step	Hyp	Ref	Expression
1		ldual0vs.f	|- F = ( LFnl ` W )
2		ldual0vs.r	|- R = ( Scalar ` W )
3		ldual0vs.z	|- .0. = ( 0g ` R )
4		ldual0vs.d	|- D = ( LDual ` W )
5		ldual0vs.t	|- .x. = ( .s ` D )
6		ldual0vs.o	|- O = ( 0g ` D )
7		ldual0vs.w	|- ( ph -> W e. LMod )
8		ldual0vs.g	|- ( ph -> G e. F )
9		eqid	|- ( Scalar ` D ) = ( Scalar ` D )
10		eqid	|- ( 0g ` ( Scalar ` D ) ) = ( 0g ` ( Scalar ` D ) )
11	2 3 4 9 10 7	ldual0	|- ( ph -> ( 0g ` ( Scalar ` D ) ) = .0. )
12	11	oveq1d	|- ( ph -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = ( .0. .x. G ) )
13	4 7	lduallmod	|- ( ph -> D e. LMod )
14		eqid	|- ( Base ` D ) = ( Base ` D )
15	1 4 14 7 8	ldualelvbase	|- ( ph -> G e. ( Base ` D ) )
16	14 9 5 10 6	lmod0vs	|- ( ( D e. LMod /\ G e. ( Base ` D ) ) -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = O )
17	13 15 16	syl2anc	|- ( ph -> ( ( 0g ` ( Scalar ` D ) ) .x. G ) = O )
18	12 17	eqtr3d	|- ( ph -> ( .0. .x. G ) = O )