Metamath Proof Explorer

Theorem tendofset

Description: The set of all trace-preserving endomorphisms on the set of translations for a lattice K . (Contributed by NM, 8-Jun-2013)

Ref Expression
Hypotheses tendoset.l 
|- .<_ = ( le ` K )
tendoset.h 
|- H = ( LHyp ` K )
Assertion tendofset 
|- ( K e. V -> ( TEndo ` K ) = ( w e. H |-> { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } ) )

Proof

Step Hyp Ref Expression
1 tendoset.l 
 |-  .<_ = ( le ` K )
2 tendoset.h 
 |-  H = ( LHyp ` K )
3 elex 
 |-  ( K e. V -> K e. _V )
4 fveq2 
 |-  ( k = K -> ( LHyp ` k ) = ( LHyp ` K ) )
5 4 2 eqtr4di 
 |-  ( k = K -> ( LHyp ` k ) = H )
6 fveq2 
 |-  ( k = K -> ( LTrn ` k ) = ( LTrn ` K ) )
7 6 fveq1d 
 |-  ( k = K -> ( ( LTrn ` k ) ` w ) = ( ( LTrn ` K ) ` w ) )
8 7 7 feq23d 
 |-  ( k = K -> ( s : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) <-> s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) ) )
9 7 raleqdv 
 |-  ( k = K -> ( A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) <-> A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) ) )
10 7 9 raleqbidv 
 |-  ( k = K -> ( A. f e. ( ( LTrn ` k ) ` w ) A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) <-> A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) ) )
11 fveq2 
 |-  ( k = K -> ( trL ` k ) = ( trL ` K ) )
12 11 fveq1d 
 |-  ( k = K -> ( ( trL ` k ) ` w ) = ( ( trL ` K ) ` w ) )
13 12 fveq1d 
 |-  ( k = K -> ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) = ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) )
14 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
15 14 1 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
16 12 fveq1d 
 |-  ( k = K -> ( ( ( trL ` k ) ` w ) ` f ) = ( ( ( trL ` K ) ` w ) ` f ) )
17 13 15 16 breq123d 
 |-  ( k = K -> ( ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) <-> ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) )
18 7 17 raleqbidv 
 |-  ( k = K -> ( A. f e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) <-> A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) )
19 8 10 18 3anbi123d 
 |-  ( k = K -> ( ( s : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. f e. ( ( LTrn ` k ) ` w ) A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) ) <-> ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) ) )
20 19 abbidv 
 |-  ( k = K -> { s | ( s : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. f e. ( ( LTrn ` k ) ` w ) A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) ) } = { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } )
21 5 20 mpteq12dv 
 |-  ( k = K -> ( w e. ( LHyp ` k ) |-> { s | ( s : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. f e. ( ( LTrn ` k ) ` w ) A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) ) } ) = ( w e. H |-> { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } ) )
22 df-tendo 
 |-  TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { s | ( s : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. f e. ( ( LTrn ` k ) ` w ) A. g e. ( ( LTrn ` k ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( s ` f ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` f ) ) } ) )
23 21 22 2 mptfvmpt 
 |-  ( K e. _V -> ( TEndo ` K ) = ( w e. H |-> { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } ) )
24 3 23 syl 
 |-  ( K e. V -> ( TEndo ` K ) = ( w e. H |-> { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } ) )