Metamath Proof Explorer

Definition df-tendo

Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013)

Ref Expression
Assertion df-tendo 
|- TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctendo 
 |-  TEndo
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vw 
 |-  w
4 clh 
 |-  LHyp
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( LHyp ` k )
7 vf 
 |-  f
8 7 cv 
 |-  f
9 cltrn 
 |-  LTrn
10 5 9 cfv 
 |-  ( LTrn ` k )
11 3 cv 
 |-  w
12 11 10 cfv 
 |-  ( ( LTrn ` k ) ` w )
13 12 12 8 wf 
 |-  f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 15 cv 
 |-  y
18 16 17 ccom 
 |-  ( x o. y )
19 18 8 cfv 
 |-  ( f ` ( x o. y ) )
20 16 8 cfv 
 |-  ( f ` x )
21 17 8 cfv 
 |-  ( f ` y )
22 20 21 ccom 
 |-  ( ( f ` x ) o. ( f ` y ) )
23 19 22 wceq 
 |-  ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
24 23 15 12 wral 
 |-  A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
25 24 14 12 wral 
 |-  A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) )
26 ctrl 
 |-  trL
27 5 26 cfv 
 |-  ( trL ` k )
28 11 27 cfv 
 |-  ( ( trL ` k ) ` w )
29 20 28 cfv 
 |-  ( ( ( trL ` k ) ` w ) ` ( f ` x ) )
30 cple 
 |-  le
31 5 30 cfv 
 |-  ( le ` k )
32 16 28 cfv 
 |-  ( ( ( trL ` k ) ` w ) ` x )
33 29 32 31 wbr 
 |-  ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x )
34 33 14 12 wral 
 |-  A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x )
35 13 25 34 w3a 
 |-  ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) )
36 35 7 cab 
 |-  { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) }
37 3 6 36 cmpt 
 |-  ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } )
38 1 2 37 cmpt 
 |-  ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )
39 0 38 wceq 
 |-  TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )