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

Definition df-ltrn 29445
Description: Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-ltrn  |-  LTrn  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { f  e.  ( (
LDil `  k ) `  w )  |  A. p  e.  ( Atoms `  k ) A. q  e.  ( Atoms `  k )
( ( -.  p
( le `  k
) w  /\  -.  q ( le `  k ) w )  ->  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )  =  ( ( q ( join `  k ) ( f `
 q ) ) ( meet `  k
) w ) ) } ) )
Distinct variable group:    w, k, f, p, q

Detailed syntax breakdown of Definition df-ltrn
StepHypRef Expression
1 cltrn 29441 . 2  class  LTrn
2 vk . . 3  set  k
3 cvv 2757 . . 3  class  _V
4 vw . . . 4  set  w
52cv 1618 . . . . 5  class  k
6 clh 29324 . . . . 5  class  LHyp
75, 6cfv 4659 . . . 4  class  ( LHyp `  k )
8 vp . . . . . . . . . . . 12  set  p
98cv 1618 . . . . . . . . . . 11  class  p
104cv 1618 . . . . . . . . . . 11  class  w
11 cple 13163 . . . . . . . . . . . 12  class  le
125, 11cfv 4659 . . . . . . . . . . 11  class  ( le
`  k )
139, 10, 12wbr 3983 . . . . . . . . . 10  wff  p ( le `  k ) w
1413wn 5 . . . . . . . . 9  wff  -.  p
( le `  k
) w
15 vq . . . . . . . . . . . 12  set  q
1615cv 1618 . . . . . . . . . . 11  class  q
1716, 10, 12wbr 3983 . . . . . . . . . 10  wff  q ( le `  k ) w
1817wn 5 . . . . . . . . 9  wff  -.  q
( le `  k
) w
1914, 18wa 360 . . . . . . . 8  wff  ( -.  p ( le `  k ) w  /\  -.  q ( le `  k ) w )
20 vf . . . . . . . . . . . . 13  set  f
2120cv 1618 . . . . . . . . . . . 12  class  f
229, 21cfv 4659 . . . . . . . . . . 11  class  ( f `
 p )
23 cjn 14026 . . . . . . . . . . . 12  class  join
245, 23cfv 4659 . . . . . . . . . . 11  class  ( join `  k )
259, 22, 24co 5778 . . . . . . . . . 10  class  ( p ( join `  k
) ( f `  p ) )
26 cmee 14027 . . . . . . . . . . 11  class  meet
275, 26cfv 4659 . . . . . . . . . 10  class  ( meet `  k )
2825, 10, 27co 5778 . . . . . . . . 9  class  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )
2916, 21cfv 4659 . . . . . . . . . . 11  class  ( f `
 q )
3016, 29, 24co 5778 . . . . . . . . . 10  class  ( q ( join `  k
) ( f `  q ) )
3130, 10, 27co 5778 . . . . . . . . 9  class  ( ( q ( join `  k
) ( f `  q ) ) (
meet `  k )
w )
3228, 31wceq 1619 . . . . . . . 8  wff  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )  =  ( ( q ( join `  k ) ( f `
 q ) ) ( meet `  k
) w )
3319, 32wi 6 . . . . . . 7  wff  ( ( -.  p ( le
`  k ) w  /\  -.  q ( le `  k ) w )  ->  (
( p ( join `  k ) ( f `
 p ) ) ( meet `  k
) w )  =  ( ( q (
join `  k )
( f `  q
) ) ( meet `  k ) w ) )
34 catm 28604 . . . . . . . 8  class  Atoms
355, 34cfv 4659 . . . . . . 7  class  ( Atoms `  k )
3633, 15, 35wral 2516 . . . . . 6  wff  A. q  e.  ( Atoms `  k )
( ( -.  p
( le `  k
) w  /\  -.  q ( le `  k ) w )  ->  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )  =  ( ( q ( join `  k ) ( f `
 q ) ) ( meet `  k
) w ) )
3736, 8, 35wral 2516 . . . . 5  wff  A. p  e.  ( Atoms `  k ) A. q  e.  ( Atoms `  k ) ( ( -.  p ( le `  k ) w  /\  -.  q
( le `  k
) w )  -> 
( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w )  =  ( ( q ( join `  k
) ( f `  q ) ) (
meet `  k )
w ) )
38 cldil 29440 . . . . . . 7  class  LDil
395, 38cfv 4659 . . . . . 6  class  ( LDil `  k )
4010, 39cfv 4659 . . . . 5  class  ( (
LDil `  k ) `  w )
4137, 20, 40crab 2520 . . . 4  class  { f  e.  ( ( LDil `  k ) `  w
)  |  A. p  e.  ( Atoms `  k ) A. q  e.  ( Atoms `  k ) ( ( -.  p ( le `  k ) w  /\  -.  q
( le `  k
) w )  -> 
( ( p (
join `  k )
( f `  p
) ) ( meet `  k ) w )  =  ( ( q ( join `  k
) ( f `  q ) ) (
meet `  k )
w ) ) }
424, 7, 41cmpt 4037 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { f  e.  ( ( LDil `  k
) `  w )  |  A. p  e.  (
Atoms `  k ) A. q  e.  ( Atoms `  k ) ( ( -.  p ( le
`  k ) w  /\  -.  q ( le `  k ) w )  ->  (
( p ( join `  k ) ( f `
 p ) ) ( meet `  k
) w )  =  ( ( q (
join `  k )
( f `  q
) ) ( meet `  k ) w ) ) } )
432, 3, 42cmpt 4037 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { f  e.  ( ( LDil `  k
) `  w )  |  A. p  e.  (
Atoms `  k ) A. q  e.  ( Atoms `  k ) ( ( -.  p ( le
`  k ) w  /\  -.  q ( le `  k ) w )  ->  (
( p ( join `  k ) ( f `
 p ) ) ( meet `  k
) w )  =  ( ( q (
join `  k )
( f `  q
) ) ( meet `  k ) w ) ) } ) )
441, 43wceq 1619 1  wff  LTrn  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { f  e.  ( (
LDil `  k ) `  w )  |  A. p  e.  ( Atoms `  k ) A. q  e.  ( Atoms `  k )
( ( -.  p
( le `  k
) w  /\  -.  q ( le `  k ) w )  ->  ( ( p ( join `  k
) ( f `  p ) ) (
meet `  k )
w )  =  ( ( q ( join `  k ) ( f `
 q ) ) ( meet `  k
) w ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  ltrnfset  29457
  Copyright terms: Public domain W3C validator