Metamath Proof Explorer

Definition df-dilN

Description: Define set of all dilations. Definition of dilation in Crawley p. 111. (Contributed by NM, 30-Jan-2012)

Ref Expression
Assertion 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 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdilN 
 |-  Dil
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vd 
 |-  d
4 catm 
 |-  Atoms
5 1 cv 
 |-  k
6 5 4 cfv 
 |-  ( Atoms ` k )
7 vf 
 |-  f
8 cpautN 
 |-  PAut
9 5 8 cfv 
 |-  ( PAut ` k )
10 vx 
 |-  x
11 cpsubsp 
 |-  PSubSp
12 5 11 cfv 
 |-  ( PSubSp ` k )
13 10 cv 
 |-  x
14 cwpointsN 
 |-  WAtoms
15 5 14 cfv 
 |-  ( WAtoms ` k )
16 3 cv 
 |-  d
17 16 15 cfv 
 |-  ( ( WAtoms ` k ) ` d )
18 13 17 wss 
 |-  x C_ ( ( WAtoms ` k ) ` d )
19 7 cv 
 |-  f
20 13 19 cfv 
 |-  ( f ` x )
21 20 13 wceq 
 |-  ( f ` x ) = x
22 18 21 wi 
 |-  ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x )
23 22 10 12 wral 
 |-  A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x )
24 23 7 9 crab 
 |-  { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) }
25 3 6 24 cmpt 
 |-  ( d e. ( Atoms ` k ) |-> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } )
26 1 2 25 cmpt 
 |-  ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } ) )
27 0 26 wceq 
 |-  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 ) } ) )