Theorem hlhilipval

Description: Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilip.h	|- H = ( LHyp ` K )
	hlhilip.l	|- L = ( ( DVecH ` K ) ` W )
	hlhilip.v	|- V = ( Base ` L )
	hlhilip.s	|- S = ( ( HDMap ` K ) ` W )
	hlhilip.u	|- U = ( ( HLHil ` K ) ` W )
	hlhilip.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hlhilip.i	|- ., = ( .i ` U )
	hlhilip.x	|- ( ph -> X e. V )
	hlhilip.y	|- ( ph -> Y e. V )
Assertion	hlhilipval	|- ( ph -> ( X ., Y ) = ( ( S ` Y ) ` X ) )

Proof

Step	Hyp	Ref	Expression
1		hlhilip.h	|- H = ( LHyp ` K )
2		hlhilip.l	|- L = ( ( DVecH ` K ) ` W )
3		hlhilip.v	|- V = ( Base ` L )
4		hlhilip.s	|- S = ( ( HDMap ` K ) ` W )
5		hlhilip.u	|- U = ( ( HLHil ` K ) ` W )
6		hlhilip.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7		hlhilip.i	|- ., = ( .i ` U )
8		hlhilip.x	|- ( ph -> X e. V )
9		hlhilip.y	|- ( ph -> Y e. V )
10		eqid	|- ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )
11	1 2 3 4 5 6 10	hlhilip	|- ( ph -> ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) = ( .i ` U ) )
12	7 11	eqtr4id	|- ( ph -> ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) )
13	12	oveqd	|- ( ph -> ( X ., Y ) = ( X ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) Y ) )
14		fveq2	|- ( x = X -> ( ( S ` y ) ` x ) = ( ( S ` y ) ` X ) )
15		fveq2	|- ( y = Y -> ( S ` y ) = ( S ` Y ) )
16	15	fveq1d	|- ( y = Y -> ( ( S ` y ) ` X ) = ( ( S ` Y ) ` X ) )
17		fvex	|- ( ( S ` Y ) ` X ) e. _V
18	14 16 10 17	ovmpo	|- ( ( X e. V /\ Y e. V ) -> ( X ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) Y ) = ( ( S ` Y ) ` X ) )
19	8 9 18	syl2anc	|- ( ph -> ( X ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) Y ) = ( ( S ` Y ) ` X ) )
20	13 19	eqtrd	|- ( ph -> ( X ., Y ) = ( ( S ` Y ) ` X ) )