Metamath Proof Explorer

Theorem hlhilplus

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