Metamath Proof Explorer

Theorem hlhilvsca

Description: The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilvsca.h 
|- H = ( LHyp ` K )
hlhilvsca.l 
|- L = ( ( DVecH ` K ) ` W )
hlhilvsca.t 
|- .x. = ( .s ` L )
hlhilvsca.u 
|- U = ( ( HLHil ` K ) ` W )
hlhilvsca.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hlhilvsca 
|- ( ph -> .x. = ( .s ` U ) )

Proof

Step Hyp Ref Expression
1 hlhilvsca.h 
 |-  H = ( LHyp ` K )
2 hlhilvsca.l 
 |-  L = ( ( DVecH ` K ) ` W )
3 hlhilvsca.t 
 |-  .x. = ( .s ` L )
4 hlhilvsca.u 
 |-  U = ( ( HLHil ` K ) ` W )
5 hlhilvsca.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 3 fvexi 
 |-  .x. e. _V
7 eqid 
 |-  ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } )
8 7 phlvsca 
 |-  ( .x. e. _V -> .x. = ( .s ` ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) ) )
9 6 8 ax-mp 
 |-  .x. = ( .s ` ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) )
10 eqid 
 |-  ( Base ` L ) = ( Base ` L )
11 eqid 
 |-  ( +g ` L ) = ( +g ` L )
12 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
13 eqid 
 |-  ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
14 eqid 
 |-  ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. )
15 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
16 eqid 
 |-  ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) = ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) )
17 1 4 2 10 11 12 13 14 3 15 16 5 hlhilset 
 |-  ( ph -> U = ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) )
18 17 fveq2d 
 |-  ( ph -> ( .s ` U ) = ( .s ` ( { <. ( Base ` ndx ) , ( Base ` L ) >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ( x e. ( Base ` L ) , y e. ( Base ` L ) |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) ) )
19 9 18 eqtr4id 
 |-  ( ph -> .x. = ( .s ` U ) )