Metamath Proof Explorer

Theorem tendoset

Description: The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom W . (Contributed by NM, 8-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 tendoset.l 
 |-  .<_ = ( le ` K )
2 tendoset.h 
 |-  H = ( LHyp ` K )
3 tendoset.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 tendoset.r 
 |-  R = ( ( trL ` K ) ` W )
5 tendoset.e 
 |-  E = ( ( TEndo ` K ) ` W )
6 1 2 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 ) ) } ) )
7 6 fveq1d 
 |-  ( K e. V -> ( ( TEndo ` K ) ` W ) = ( ( 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 ) ) } ) ` W ) )
8 fveq2 
 |-  ( w = W -> ( ( LTrn ` K ) ` w ) = ( ( LTrn ` K ) ` W ) )
9 8 8 feq23d 
 |-  ( w = W -> ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) <-> s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) ) )
10 8 raleqdv 
 |-  ( w = W -> ( 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 ) ) ) )
11 8 10 raleqbidv 
 |-  ( w = 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 ) A. g e. ( ( LTrn ` K ) ` W ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) ) )
12 fveq2 
 |-  ( w = W -> ( ( trL ` K ) ` w ) = ( ( trL ` K ) ` W ) )
13 12 4 eqtr4di 
 |-  ( w = W -> ( ( trL ` K ) ` w ) = R )
14 13 fveq1d 
 |-  ( w = W -> ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) = ( R ` ( s ` f ) ) )
15 13 fveq1d 
 |-  ( w = W -> ( ( ( trL ` K ) ` w ) ` f ) = ( R ` f ) )
16 14 15 breq12d 
 |-  ( w = W -> ( ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) <-> ( R ` ( s ` f ) ) .<_ ( R ` f ) ) )
17 8 16 raleqbidv 
 |-  ( w = W -> ( A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) <-> A. f e. ( ( LTrn ` K ) ` W ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) )
18 9 11 17 3anbi123d 
 |-  ( w = W -> ( ( 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 ) ) <-> ( 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) ) )
19 18 abbidv 
 |-  ( w = W -> { 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 ) ) } = { 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
20 eqid 
 |-  ( 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 ) ) } ) = ( 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 ) ) } )
21 fvex 
 |-  ( ( LTrn ` K ) ` W ) e. _V
22 21 21 mapval 
 |-  ( ( ( LTrn ` K ) ` W ) ^m ( ( LTrn ` K ) ` W ) ) = { s | s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) }
23 ovex 
 |-  ( ( ( LTrn ` K ) ` W ) ^m ( ( LTrn ` K ) ` W ) ) e. _V
24 22 23 eqeltrri 
 |-  { s | s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) } e. _V
25 simp1 
 |-  ( ( 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) -> s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) )
26 25 ss2abi 
 |-  { 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } C_ { s | s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) }
27 24 26 ssexi 
 |-  { 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } e. _V
28 19 20 27 fvmpt 
 |-  ( W e. H -> ( ( 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 ) ) } ) ` W ) = { 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
29 3 3 feq23i 
 |-  ( s : T --> T <-> s : ( ( LTrn ` K ) ` W ) --> ( ( LTrn ` K ) ` W ) )
30 3 raleqi 
 |-  ( A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) <-> A. g e. ( ( LTrn ` K ) ` W ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) )
31 3 30 raleqbii 
 |-  ( A. f e. T A. g e. T ( 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 ) ) )
32 3 raleqi 
 |-  ( A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) <-> A. f e. ( ( LTrn ` K ) ` W ) ( R ` ( s ` f ) ) .<_ ( R ` f ) )
33 29 31 32 3anbi123i 
 |-  ( ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) )
34 33 abbii 
 |-  { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` 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 ) ( R ` ( s ` f ) ) .<_ ( R ` f ) ) }
35 28 34 eqtr4di 
 |-  ( W e. H -> ( ( 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 ) ) } ) ` W ) = { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
36 7 35 sylan9eq 
 |-  ( ( K e. V /\ W e. H ) -> ( ( TEndo ` K ) ` W ) = { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
37 5 36 syl5eq 
 |-  ( ( K e. V /\ W e. H ) -> E = { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )