Theorem lcd0vs

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

	Ref	Expression
Hypotheses	lcd0vs.h	|- H = ( LHyp ` K )
	lcd0vs.u	|- U = ( ( DVecH ` K ) ` W )
	lcd0vs.r	|- R = ( Scalar ` U )
	lcd0vs.z	|- .0. = ( 0g ` R )
	lcd0vs.c	|- C = ( ( LCDual ` K ) ` W )
	lcd0vs.v	|- V = ( Base ` C )
	lcd0vs.t	|- .x. = ( .s ` C )
	lcd0vs.o	|- O = ( 0g ` C )
	lcd0vs.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcd0vs.g	|- ( ph -> G e. V )
Assertion	lcd0vs	|- ( ph -> ( .0. .x. G ) = O )

Proof

Step	Hyp	Ref	Expression
1		lcd0vs.h	|- H = ( LHyp ` K )
2		lcd0vs.u	|- U = ( ( DVecH ` K ) ` W )
3		lcd0vs.r	|- R = ( Scalar ` U )
4		lcd0vs.z	|- .0. = ( 0g ` R )
5		lcd0vs.c	|- C = ( ( LCDual ` K ) ` W )
6		lcd0vs.v	|- V = ( Base ` C )
7		lcd0vs.t	|- .x. = ( .s ` C )
8		lcd0vs.o	|- O = ( 0g ` C )
9		lcd0vs.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcd0vs.g	|- ( ph -> G e. V )
11		eqid	|- ( Scalar ` C ) = ( Scalar ` C )
12		eqid	|- ( 0g ` ( Scalar ` C ) ) = ( 0g ` ( Scalar ` C ) )
13	1 2 3 4 5 11 12 9	lcd0	|- ( ph -> ( 0g ` ( Scalar ` C ) ) = .0. )
14	13	oveq1d	|- ( ph -> ( ( 0g ` ( Scalar ` C ) ) .x. G ) = ( .0. .x. G ) )
15	1 5 9	lcdlmod	|- ( ph -> C e. LMod )
16	6 11 7 12 8	lmod0vs	|- ( ( C e. LMod /\ G e. V ) -> ( ( 0g ` ( Scalar ` C ) ) .x. G ) = O )
17	15 10 16	syl2anc	|- ( ph -> ( ( 0g ` ( Scalar ` C ) ) .x. G ) = O )
18	14 17	eqtr3d	|- ( ph -> ( .0. .x. G ) = O )