Theorem lcdvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 20-Mar-2015)

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

Proof

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