Theorem ldualvscl

Description: The scalar product operation value is a functional. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	ldualvscl.f	|- F = ( LFnl ` W )
	ldualvscl.r	|- R = ( Scalar ` W )
	ldualvscl.k	|- K = ( Base ` R )
	ldualvscl.d	|- D = ( LDual ` W )
	ldualvscl.s	|- .x. = ( .s ` D )
	ldualvscl.w	|- ( ph -> W e. LMod )
	ldualvscl.x	|- ( ph -> X e. K )
	ldualvscl.g	|- ( ph -> G e. F )
Assertion	ldualvscl	|- ( ph -> ( X .x. G ) e. F )

Proof

Step	Hyp	Ref	Expression
1		ldualvscl.f	|- F = ( LFnl ` W )
2		ldualvscl.r	|- R = ( Scalar ` W )
3		ldualvscl.k	|- K = ( Base ` R )
4		ldualvscl.d	|- D = ( LDual ` W )
5		ldualvscl.s	|- .x. = ( .s ` D )
6		ldualvscl.w	|- ( ph -> W e. LMod )
7		ldualvscl.x	|- ( ph -> X e. K )
8		ldualvscl.g	|- ( ph -> G e. F )
9		eqid	|- ( Base ` W ) = ( Base ` W )
10		eqid	|- ( .r ` R ) = ( .r ` R )
11	1 9 2 3 10 4 5 6 7 8	ldualvs	|- ( ph -> ( X .x. G ) = ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) )
12	9 2 3 10 1 6 8 7	lflvscl	|- ( ph -> ( G oF ( .r ` R ) ( ( Base ` W ) X. { X } ) ) e. F )
13	11 12	eqeltrd	|- ( ph -> ( X .x. G ) e. F )