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

Definition df-dilN 30917
Description: Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.)
Assertion
Ref Expression
df-dilN  |-  Dil  =  ( k  e.  _V  |->  ( d  e.  (
Atoms `  k )  |->  { f  e.  ( PAut `  k )  |  A. x  e.  ( PSubSp `  k ) ( x 
C_  ( ( WAtoms `  k ) `  d
)  ->  ( f `  x )  =  x ) } ) )
Distinct variable group:    k, d, f, x

Detailed syntax breakdown of Definition df-dilN
StepHypRef Expression
1 cdilN 30913 . 2  class  Dil
2 vk . . 3  set  k
3 cvv 2801 . . 3  class  _V
4 vd . . . 4  set  d
52cv 1631 . . . . 5  class  k
6 catm 30075 . . . . 5  class  Atoms
75, 6cfv 5271 . . . 4  class  ( Atoms `  k )
8 vx . . . . . . . . 9  set  x
98cv 1631 . . . . . . . 8  class  x
104cv 1631 . . . . . . . . 9  class  d
11 cwpointsN 30797 . . . . . . . . . 10  class  WAtoms
125, 11cfv 5271 . . . . . . . . 9  class  ( WAtoms `  k )
1310, 12cfv 5271 . . . . . . . 8  class  ( (
WAtoms `  k ) `  d )
149, 13wss 3165 . . . . . . 7  wff  x  C_  ( ( WAtoms `  k
) `  d )
15 vf . . . . . . . . . 10  set  f
1615cv 1631 . . . . . . . . 9  class  f
179, 16cfv 5271 . . . . . . . 8  class  ( f `
 x )
1817, 9wceq 1632 . . . . . . 7  wff  ( f `
 x )  =  x
1914, 18wi 4 . . . . . 6  wff  ( x 
C_  ( ( WAtoms `  k ) `  d
)  ->  ( f `  x )  =  x )
20 cpsubsp 30307 . . . . . . 7  class  PSubSp
215, 20cfv 5271 . . . . . 6  class  ( PSubSp `  k )
2219, 8, 21wral 2556 . . . . 5  wff  A. x  e.  ( PSubSp `  k )
( x  C_  (
( WAtoms `  k ) `  d )  ->  (
f `  x )  =  x )
23 cpautN 30798 . . . . . 6  class  PAut
245, 23cfv 5271 . . . . 5  class  ( PAut `  k )
2522, 15, 24crab 2560 . . . 4  class  { f  e.  ( PAut `  k
)  |  A. x  e.  ( PSubSp `  k )
( x  C_  (
( WAtoms `  k ) `  d )  ->  (
f `  x )  =  x ) }
264, 7, 25cmpt 4093 . . 3  class  ( d  e.  ( Atoms `  k
)  |->  { f  e.  ( PAut `  k
)  |  A. x  e.  ( PSubSp `  k )
( x  C_  (
( WAtoms `  k ) `  d )  ->  (
f `  x )  =  x ) } )
272, 3, 26cmpt 4093 . 2  class  ( k  e.  _V  |->  ( d  e.  ( Atoms `  k
)  |->  { f  e.  ( PAut `  k
)  |  A. x  e.  ( PSubSp `  k )
( x  C_  (
( WAtoms `  k ) `  d )  ->  (
f `  x )  =  x ) } ) )
281, 27wceq 1632 1  wff  Dil  =  ( k  e.  _V  |->  ( d  e.  (
Atoms `  k )  |->  { f  e.  ( PAut `  k )  |  A. x  e.  ( PSubSp `  k ) ( x 
C_  ( ( WAtoms `  k ) `  d
)  ->  ( f `  x )  =  x ) } ) )
Colors of variables: wff set class
This definition is referenced by:  dilfsetN  30963
  Copyright terms: Public domain W3C validator