Metamath Proof Explorer

Theorem hlhilbase

Description: The base set of the final constructed Hilbert space. (Contributed by NM, 21-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 ) )
hlhilbase.l 
|- L = ( ( DVecH ` K ) ` W )
hlhilbase.m 
|- M = ( Base ` L )
Assertion hlhilbase 
|- ( ph -> M = ( Base ` 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 hlhilbase.l 
 |-  L = ( ( DVecH ` K ) ` W )
5 hlhilbase.m 
 |-  M = ( Base ` L )
6 5 fvexi 
 |-  M e. _V
7 eqid 
 |-  ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) = ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } )
8 7 phlbase 
 |-  ( M e. _V -> M = ( Base ` ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) ) )
9 6 8 ax-mp 
 |-  M = ( Base ` ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) )
10 eqid 
 |-  ( +g ` L ) = ( +g ` L )
11 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
12 eqid 
 |-  ( ( HGMap ` K ) ` W ) = ( ( HGMap ` K ) ` W )
13 eqid 
 |-  ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) = ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. )
14 eqid 
 |-  ( .s ` L ) = ( .s ` L )
15 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
16 eqid 
 |-  ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) = ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) )
17 1 2 4 5 10 11 12 13 14 15 16 3 hlhilset 
 |-  ( ph -> U = ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) )
18 17 fveq2d 
 |-  ( ph -> ( Base ` U ) = ( Base ` ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , ( +g ` L ) >. , <. ( Scalar ` ndx ) , ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , ( ( HGMap ` K ) ` W ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` L ) >. , <. ( .i ` ndx ) , ( x e. M , y e. M |-> ( ( ( ( HDMap ` K ) ` W ) ` y ) ` x ) ) >. } ) ) )
19 9 18 eqtr4id 
 |-  ( ph -> M = ( Base ` U ) )