Theorem lcdlssvscl

Description: Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcdlssvscl.h	|- H = ( LHyp ` K )
	lcdlssvscl.u	|- U = ( ( DVecH ` K ) ` W )
	lcdlssvscl.f	|- F = ( Scalar ` U )
	lcdlssvscl.r	|- R = ( Base ` F )
	lcdlssvscl.c	|- C = ( ( LCDual ` K ) ` W )
	lcdlssvscl.v	|- V = ( Base ` C )
	lcdlssvscl.t	|- .x. = ( .s ` C )
	lcdlssvscl.s	|- S = ( LSubSp ` C )
	lcdlssvscl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	lcdlssvscl.l	|- ( ph -> L e. S )
	lcdlssvscl.x	|- ( ph -> X e. R )
	lcdlssvscl.y	|- ( ph -> Y e. L )
Assertion	lcdlssvscl	|- ( ph -> ( X .x. Y ) e. L )

Proof

Step	Hyp	Ref	Expression
1		lcdlssvscl.h	|- H = ( LHyp ` K )
2		lcdlssvscl.u	|- U = ( ( DVecH ` K ) ` W )
3		lcdlssvscl.f	|- F = ( Scalar ` U )
4		lcdlssvscl.r	|- R = ( Base ` F )
5		lcdlssvscl.c	|- C = ( ( LCDual ` K ) ` W )
6		lcdlssvscl.v	|- V = ( Base ` C )
7		lcdlssvscl.t	|- .x. = ( .s ` C )
8		lcdlssvscl.s	|- S = ( LSubSp ` C )
9		lcdlssvscl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
10		lcdlssvscl.l	|- ( ph -> L e. S )
11		lcdlssvscl.x	|- ( ph -> X e. R )
12		lcdlssvscl.y	|- ( ph -> Y e. L )
13	1 5 9	lcdlmod	|- ( ph -> C e. LMod )
14		eqid	|- ( Scalar ` C ) = ( Scalar ` C )
15		eqid	|- ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
16	1 2 3 4 5 14 15 9	lcdsbase	|- ( ph -> ( Base ` ( Scalar ` C ) ) = R )
17	11 16	eleqtrrd	|- ( ph -> X e. ( Base ` ( Scalar ` C ) ) )
18	14 7 15 8	lssvscl	|- ( ( ( C e. LMod /\ L e. S ) /\ ( X e. ( Base ` ( Scalar ` C ) ) /\ Y e. L ) ) -> ( X .x. Y ) e. L )
19	13 10 17 12 18	syl22anc	|- ( ph -> ( X .x. Y ) e. L )