Metamath Proof Explorer

Theorem hlhilnvl

Description: The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

Ref Expression
Hypotheses hlhilnvl.h 
|- H = ( LHyp ` K )
hlhilnvl.u 
|- U = ( ( HLHil ` K ) ` W )
hlhilnvl.r 
|- R = ( Scalar ` U )
hlhilnvl.i 
|- .* = ( ( HGMap ` K ) ` W )
hlhilnvl.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion hlhilnvl 
|- ( ph -> .* = ( *r ` R ) )

Proof

Step Hyp Ref Expression
1 hlhilnvl.h 
 |-  H = ( LHyp ` K )
2 hlhilnvl.u 
 |-  U = ( ( HLHil ` K ) ` W )
3 hlhilnvl.r 
 |-  R = ( Scalar ` U )
4 hlhilnvl.i 
 |-  .* = ( ( HGMap ` K ) ` W )
5 hlhilnvl.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
6 fvex 
 |-  ( ( EDRing ` K ) ` W ) e. _V
7 4 fvexi 
 |-  .* e. _V
8 starvid 
 |-  *r = Slot ( *r ` ndx )
9 8 setsid 
 |-  ( ( ( ( EDRing ` K ) ` W ) e. _V /\ .* e. _V ) -> .* = ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) ) )
10 6 7 9 mp2an 
 |-  .* = ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) )
11 eqid 
 |-  ( ( EDRing ` K ) ` W ) = ( ( EDRing ` K ) ` W )
12 eqid 
 |-  ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. )
13 1 2 5 11 4 12 hlhilsca 
 |-  ( ph -> ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = ( Scalar ` U ) )
14 13 3 eqtr4di 
 |-  ( ph -> ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) = R )
15 14 fveq2d 
 |-  ( ph -> ( *r ` ( ( ( EDRing ` K ) ` W ) sSet <. ( *r ` ndx ) , .* >. ) ) = ( *r ` R ) )
16 10 15 eqtrid 
 |-  ( ph -> .* = ( *r ` R ) )