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

Definition df-trl 30348
Description: Define trace of a lattice translation. (Contributed by NM, 20-May-2012.)
Assertion
Ref Expression
df-trl  |-  trL  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( f  e.  ( (
LTrn `  k ) `  w )  |->  ( iota_ x  e.  ( Base `  k
) A. p  e.  ( Atoms `  k )
( -.  p ( le `  k ) w  ->  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w ) ) ) ) ) )
Distinct variable group:    w, k, f, x, p

Detailed syntax breakdown of Definition df-trl
StepHypRef Expression
1 ctrl 30347 . 2  class  trL
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 )
8 vf . . . . 5  set  f
94cv 1622 . . . . . 6  class  w
10 cltrn 30290 . . . . . . 7  class  LTrn
115, 10cfv 5255 . . . . . 6  class  ( LTrn `  k )
129, 11cfv 5255 . . . . 5  class  ( (
LTrn `  k ) `  w )
13 vp . . . . . . . . . . 11  set  p
1413cv 1622 . . . . . . . . . 10  class  p
15 cple 13215 . . . . . . . . . . 11  class  le
165, 15cfv 5255 . . . . . . . . . 10  class  ( le
`  k )
1714, 9, 16wbr 4023 . . . . . . . . 9  wff  p ( le `  k ) w
1817wn 3 . . . . . . . 8  wff  -.  p
( le `  k
) w
19 vx . . . . . . . . . 10  set  x
2019cv 1622 . . . . . . . . 9  class  x
218cv 1622 . . . . . . . . . . . 12  class  f
2214, 21cfv 5255 . . . . . . . . . . 11  class  ( f `
 p )
23 cjn 14078 . . . . . . . . . . . 12  class  join
245, 23cfv 5255 . . . . . . . . . . 11  class  ( join `  k )
2514, 22, 24co 5858 . . . . . . . . . 10  class  ( p ( join `  k
) ( f `  p ) )
26 cmee 14079 . . . . . . . . . . 11  class  meet
275, 26cfv 5255 . . . . . . . . . 10  class  ( meet `  k )
2825, 9, 27co 5858 . . . . . . . . 9  class  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )
2920, 28wceq 1623 . . . . . . . 8  wff  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w )
3018, 29wi 4 . . . . . . 7  wff  ( -.  p ( le `  k ) w  ->  x  =  ( (
p ( join `  k
) ( f `  p ) ) (
meet `  k )
w ) )
31 catm 29453 . . . . . . . 8  class  Atoms
325, 31cfv 5255 . . . . . . 7  class  ( Atoms `  k )
3330, 13, 32wral 2543 . . . . . 6  wff  A. p  e.  ( Atoms `  k )
( -.  p ( le `  k ) w  ->  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w ) )
34 cbs 13148 . . . . . . 7  class  Base
355, 34cfv 5255 . . . . . 6  class  ( Base `  k )
3633, 19, 35crio 6297 . . . . 5  class  ( iota_ x  e.  ( Base `  k
) A. p  e.  ( Atoms `  k )
( -.  p ( le `  k ) w  ->  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w ) ) )
378, 12, 36cmpt 4077 . . . 4  class  ( f  e.  ( ( LTrn `  k ) `  w
)  |->  ( iota_ x  e.  ( Base `  k
) A. p  e.  ( Atoms `  k )
( -.  p ( le `  k ) w  ->  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w ) ) ) )
384, 7, 37cmpt 4077 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  ( f  e.  ( ( LTrn `  k
) `  w )  |->  ( iota_ x  e.  (
Base `  k ) A. p  e.  ( Atoms `  k ) ( -.  p ( le
`  k ) w  ->  x  =  ( ( p ( join `  k ) ( f `
 p ) ) ( meet `  k
) w ) ) ) ) )
392, 3, 38cmpt 4077 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  ( f  e.  ( ( LTrn `  k
) `  w )  |->  ( iota_ x  e.  (
Base `  k ) A. p  e.  ( Atoms `  k ) ( -.  p ( le
`  k ) w  ->  x  =  ( ( p ( join `  k ) ( f `
 p ) ) ( meet `  k
) w ) ) ) ) ) )
401, 39wceq 1623 1  wff  trL  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  ( f  e.  ( (
LTrn `  k ) `  w )  |->  ( iota_ x  e.  ( Base `  k
) A. p  e.  ( Atoms `  k )
( -.  p ( le `  k ) w  ->  x  =  ( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  trlfset  30349
  Copyright terms: Public domain W3C validator