Theorem lcdvs0N

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

	Ref	Expression
Hypotheses	lcdvs0.h	|- H = ( LHyp ` K )
	lcdvs0.u	|- U = ( ( DVecH ` K ) ` W )
	lcdvs0.s	|- S = ( Scalar ` U )
	lcdvs0.r	|- R = ( Base ` S )
	lcdvs0.c	|- C = ( ( LCDual ` K ) ` W )
	lcdvs0.t	|- .x. = ( .s ` C )
	lcdvs0.o	|- .0. = ( 0g ` C )
	lcdvs0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdvs0.x	|- ( ph -> X e. R )
Assertion	lcdvs0N	|- ( ph -> ( X .x. .0. ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lcdvs0.h	|- H = ( LHyp ` K )
2		lcdvs0.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdvs0.s	|- S = ( Scalar ` U )
4		lcdvs0.r	|- R = ( Base ` S )
5		lcdvs0.c	|- C = ( ( LCDual ` K ) ` W )
6		lcdvs0.t	|- .x. = ( .s ` C )
7		lcdvs0.o	|- .0. = ( 0g ` C )
8		lcdvs0.k	|- ( ph -> ( K e. HL /\ W e. H ) )
9		lcdvs0.x	|- ( ph -> X e. R )
10	1 5 8	lcdlmod	|- ( ph -> C e. LMod )
11		eqid	|- ( Scalar ` C ) = ( Scalar ` C )
12		eqid	|- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
13	1 2 3 4 5 11 12 8	lcdsbase	|- ( ph -> ( Base ` ( Scalar ` C ) ) = R )
14	9 13	eleqtrrd	|- ( ph -> X e. ( Base ` ( Scalar ` C ) ) )
15	11 6 12 7	lmodvs0	|- ( ( C e. LMod /\ X e. ( Base ` ( Scalar ` C ) ) ) -> ( X .x. .0. ) = .0. )
16	10 14 15	syl2anc	|- ( ph -> ( X .x. .0. ) = .0. )