Definition df-dilN 35392

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

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

This definition is referenced by:  dilfsetN  35439