Metamath Proof Explorer

Theorem hlhilip

Description: 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.p 
|- ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )
Assertion hlhilip 
|- ( ph -> ., = ( .i ` U ) )

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.p 
 |-  ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )
8 3 fvexi 
 |-  V e. _V
9 8 8 mpoex 
 |-  ( x e. V , y e. V |-> ( ( S ` y ) ` x ) ) e. _V
10 7 9 eqeltri 
 |-  ., e. _V
11 eqid 
 |-  ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } ) = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } )
12 11 phlip 
 |-  ( ., e. _V -> ., = ( .i ` ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } ) ) )
13 10 12 ax-mp 
 |-  ., = ( .i ` ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } ) )
14 eqid 
 |-  ( +g ` L ) = ( +g ` L )
15 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
16 eqid 
 |-  ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
17 eqid 
 |-  ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. )
18 eqid 
 |-  ( .s ` L ) = ( .s ` L )
19 1 5 2 3 14 15 16 17 18 4 7 6 hlhilset 
 |-  ( ph -> U = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } ) )
20 19 fveq2d 
 |-  ( ph -> ( .i ` U ) = ( .i ` ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ., >. } ) ) )
21 13 20 eqtr4id 
 |-  ( ph -> ., = ( .i ` U ) )