Theorem ldualssvscl

Description: Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015)

	Ref	Expression
Hypotheses	ldualssvscl.r	|- R = ( Scalar ` W )
	ldualssvscl.k	|- K = ( Base ` R )
	ldualssvscl.d	|- D = ( LDual ` W )
	ldualssvscl.t	|- .x. = ( .s ` D )
	ldualssvscl.s	|- S = ( LSubSp ` D )
	ldualssvscl.w	|- ( ph -> W e. LMod )
	ldualssvscl.u	|- ( ph -> U e. S )
	ldualssvscl.x	|- ( ph -> X e. K )
	ldualssvscl.y	|- ( ph -> Y e. U )
Assertion	ldualssvscl	|- ( ph -> ( X .x. Y ) e. U )

Proof

Step	Hyp	Ref	Expression
1		ldualssvscl.r	|- R = ( Scalar ` W )
2		ldualssvscl.k	|- K = ( Base ` R )
3		ldualssvscl.d	|- D = ( LDual ` W )
4		ldualssvscl.t	|- .x. = ( .s ` D )
5		ldualssvscl.s	|- S = ( LSubSp ` D )
6		ldualssvscl.w	|- ( ph -> W e. LMod )
7		ldualssvscl.u	|- ( ph -> U e. S )
8		ldualssvscl.x	|- ( ph -> X e. K )
9		ldualssvscl.y	|- ( ph -> Y e. U )
10	3 6	lduallmod	|- ( ph -> D e. LMod )
11		eqid	|- ( Scalar ` D ) = ( Scalar ` D )
12		eqid	|- ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
13	1 2 3 11 12 6	ldualsbase	|- ( ph -> ( Base ` ( Scalar ` D ) ) = K )
14	8 13	eleqtrrd	|- ( ph -> X e. ( Base ` ( Scalar ` D ) ) )
15	11 4 12 5	lssvscl	|- ( ( ( D e. LMod /\ U e. S ) /\ ( X e. ( Base ` ( Scalar ` D ) ) /\ Y e. U ) ) -> ( X .x. Y ) e. U )
16	10 7 14 9 15	syl22anc	|- ( ph -> ( X .x. Y ) e. U )