This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erngfset

Description: The division rings on trace-preserving endomorphisms for a lattice K . (Contributed by NM, 8-Jun-2013)

Ref Expression
Hypothesis erngset.h 
|- H = ( LHyp ` K )
Assertion erngfset 
|- ( K e. V -> ( EDRing ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } ) )

Proof

Step Hyp Ref Expression
1 erngset.h 
 |-  H = ( LHyp ` K )
2 elex 
 |-  ( K e. V -> K e. _V )
3 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
4 3 1 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
5 fveq2 
 |-  ( k = K -> ( TEndo ` k ) = ( TEndo ` K ) )
6 5 fveq1d 
 |-  ( k = K -> ( ( TEndo ` k ) ` w ) = ( ( TEndo ` K ) ` w ) )
7 6 opeq2d 
 |-  ( k = K -> <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. = <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. )
8 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
9 8 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
10 9 mpteq1d 
 |-  ( k = K -> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) = ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) )
11 6 6 10 mpoeq123dv 
 |-  ( k = K -> ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) = ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
12 11 opeq2d 
 |-  ( k = K -> <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. = <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. )
13 eqidd 
 |-  ( k = K -> ( s o. t ) = ( s o. t ) )
14 6 6 13 mpoeq123dv 
 |-  ( k = K -> ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) = ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) )
15 14 opeq2d 
 |-  ( k = K -> <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >. = <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. )
16 7 12 15 tpeq123d 
 |-  ( k = K -> { <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >. } = { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } )
17 4 16 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >. } ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } ) )
18 df-edring 
 |-  EDRing = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >. } ) )
19 17 18 1 mptfvmpt 
 |-  ( K e. _V -> ( EDRing ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } ) )
20 2 19 syl 
 |-  ( K e. V -> ( EDRing ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } ) )