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

Definition df-ldil 33361
Description: Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-ldil  |-  LDil  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { f  e.  ( LAut `  k )  |  A. x  e.  ( Base `  k ) ( x ( le `  k
) w  ->  (
f `  x )  =  x ) } ) )
Distinct variable group:    w, k, f, x

Detailed syntax breakdown of Definition df-ldil
StepHypRef Expression
1 cldil 33357 . 2  class  LDil
2 vk . . 3  setvar  k
3 cvv 2964 . . 3  class  _V
4 vw . . . 4  setvar  w
52cv 1363 . . . . 5  class  k
6 clh 33241 . . . . 5  class  LHyp
75, 6cfv 5408 . . . 4  class  ( LHyp `  k )
8 vx . . . . . . . . 9  setvar  x
98cv 1363 . . . . . . . 8  class  x
104cv 1363 . . . . . . . 8  class  w
11 cple 14230 . . . . . . . . 9  class  le
125, 11cfv 5408 . . . . . . . 8  class  ( le
`  k )
139, 10, 12wbr 4282 . . . . . . 7  wff  x ( le `  k ) w
14 vf . . . . . . . . . 10  setvar  f
1514cv 1363 . . . . . . . . 9  class  f
169, 15cfv 5408 . . . . . . . 8  class  ( f `
 x )
1716, 9wceq 1364 . . . . . . 7  wff  ( f `
 x )  =  x
1813, 17wi 4 . . . . . 6  wff  ( x ( le `  k
) w  ->  (
f `  x )  =  x )
19 cbs 14159 . . . . . . 7  class  Base
205, 19cfv 5408 . . . . . 6  class  ( Base `  k )
2118, 8, 20wral 2707 . . . . 5  wff  A. x  e.  ( Base `  k
) ( x ( le `  k ) w  ->  ( f `  x )  =  x )
22 claut 33242 . . . . . 6  class  LAut
235, 22cfv 5408 . . . . 5  class  ( LAut `  k )
2421, 14, 23crab 2711 . . . 4  class  { f  e.  ( LAut `  k
)  |  A. x  e.  ( Base `  k
) ( x ( le `  k ) w  ->  ( f `  x )  =  x ) }
254, 7, 24cmpt 4340 . . 3  class  ( w  e.  ( LHyp `  k
)  |->  { f  e.  ( LAut `  k
)  |  A. x  e.  ( Base `  k
) ( x ( le `  k ) w  ->  ( f `  x )  =  x ) } )
262, 3, 25cmpt 4340 . 2  class  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k
)  |->  { f  e.  ( LAut `  k
)  |  A. x  e.  ( Base `  k
) ( x ( le `  k ) w  ->  ( f `  x )  =  x ) } ) )
271, 26wceq 1364 1  wff  LDil  =  ( k  e.  _V  |->  ( w  e.  ( LHyp `  k )  |->  { f  e.  ( LAut `  k )  |  A. x  e.  ( Base `  k ) ( x ( le `  k
) w  ->  (
f `  x )  =  x ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  ldilfset  33365
  Copyright terms: Public domain W3C validator