Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-tendo Unicode version

Definition df-tendo 30944
Description: Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.)
Assertion
Ref Expression
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 )
) } ) )
Distinct variable group:    w, k, f, x, y

Detailed syntax breakdown of Definition df-tendo
StepHypRef Expression
1 ctendo 30941 . 2  class  TEndo
2 vk . . 3  set  k
3 cvv 2788 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1622 . . . . 5  class  k
6 clh 30173 . . . . 5  class  LHyp
75, 6cfv 5255 . . . 4  class  ( LHyp `  k )
84cv 1622 . . . . . . . 8  class  w
9 cltrn 30290 . . . . . . . . 9  class  LTrn
105, 9cfv 5255 . . . . . . . 8  class  ( LTrn `  k )
118, 10cfv 5255 . . . . . . 7  class  ( (
LTrn `  k ) `  w )
12 vf . . . . . . . 8  set  f
1312cv 1622 . . . . . . 7  class  f
1411, 11, 13wf 5251 . . . . . 6  wff  f : ( ( LTrn `  k
) `  w ) --> ( ( LTrn `  k
) `  w )
15 vx . . . . . . . . . . . 12  set  x
1615cv 1622 . . . . . . . . . . 11  class  x
17 vy . . . . . . . . . . . 12  set  y
1817cv 1622 . . . . . . . . . . 11  class  y
1916, 18ccom 4693 . . . . . . . . . 10  class  ( x  o.  y )
2019, 13cfv 5255 . . . . . . . . 9  class  ( f `
 ( x  o.  y ) )
2116, 13cfv 5255 . . . . . . . . . 10  class  ( f `
 x )
2218, 13cfv 5255 . . . . . . . . . 10  class  ( f `
 y )
2321, 22ccom 4693 . . . . . . . . 9  class  ( ( f `  x )  o.  ( f `  y ) )
2420, 23wceq 1623 . . . . . . . 8  wff  ( f `
 ( x  o.  y ) )  =  ( ( f `  x )  o.  (
f `  y )
)
2524, 17, 11wral 2543 . . . . . . 7  wff  A. y  e.  ( ( LTrn `  k
) `  w )
( f `  (
x  o.  y ) )  =  ( ( f `  x )  o.  ( f `  y ) )
2625, 15, 11wral 2543 . . . . . 6  wff  A. x  e.  ( ( LTrn `  k
) `  w ) A. y  e.  (
( LTrn `  k ) `  w ) ( f `
 ( x  o.  y ) )  =  ( ( f `  x )  o.  (
f `  y )
)
27 ctrl 30347 . . . . . . . . . . 11  class  trL
285, 27cfv 5255 . . . . . . . . . 10  class  ( trL `  k )
298, 28cfv 5255 . . . . . . . . 9  class  ( ( trL `  k ) `
 w )
3021, 29cfv 5255 . . . . . . . 8  class  ( ( ( trL `  k
) `  w ) `  ( f `  x
) )
3116, 29cfv 5255 . . . . . . . 8  class  ( ( ( trL `  k
) `  w ) `  x )
32 cple 13215 . . . . . . . . 9  class  le
335, 32cfv 5255 . . . . . . . 8  class  ( le
`  k )
3430, 31, 33wbr 4023 . . . . . . 7  wff  ( ( ( trL `  k
) `  w ) `  ( f `  x
) ) ( le
`  k ) ( ( ( trL `  k
) `  w ) `  x )
3534, 15, 11wral 2543 . . . . . 6  wff  A. x  e.  ( ( LTrn `  k
) `  w )
( ( ( trL `  k ) `  w
) `  ( f `  x ) ) ( le `  k ) ( ( ( trL `  k ) `  w
) `  x )
3614, 26, 35w3a 934 . . . . 5  wff  ( 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 )
)
3736, 12cab 2269 . . . 4  class  { 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 )
) }
384, 7, 37cmpt 4077 . . 3  class  ( 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 )
) } )
392, 3, 38cmpt 4077 . 2  class  ( 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 )
) } ) )
401, 39wceq 1623 1  wff  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 )
) } ) )
Colors of variables: wff set class
This definition is referenced by:  tendofset  30947
  Copyright terms: Public domain W3C validator