Metamath Proof Explorer

Theorem hlhilsca

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

Ref Expression
Hypotheses hlhilbase.h 
|- H = ( LHyp ` K )
hlhilbase.u 
|- U = ( ( HLHil ` K ) ` W )
hlhilbase.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhilsca.e 
|- E = ( ( EDRing ` K ) ` W )
hlhilsca.g 
|- G = ( ( HGMap ` K ) ` W )
hlhilsca.r 
|- R = ( E sSet <. ( *r ` ndx ) , G >. )
Assertion hlhilsca 
|- ( ph -> R = ( Scalar ` U ) )

Proof

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