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 = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdilN	⊢ Dil
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vd	⊢ 𝑑
4		catm	⊢ Atoms
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Atoms ‘ 𝑘 )
7		vf	⊢ 𝑓
8		cpautN	⊢ PAut
9	5 8	cfv	⊢ ( PAut ‘ 𝑘 )
10		vx	⊢ 𝑥
11		cpsubsp	⊢ PSubSp
12	5 11	cfv	⊢ ( PSubSp ‘ 𝑘 )
13	10	cv	⊢ 𝑥
14		cwpointsN	⊢ WAtoms
15	5 14	cfv	⊢ ( WAtoms ‘ 𝑘 )
16	3	cv	⊢ 𝑑
17	16 15	cfv	⊢ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 )
18	13 17	wss	⊢ 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 )
19	7	cv	⊢ 𝑓
20	13 19	cfv	⊢ ( 𝑓 ‘ 𝑥 )
21	20 13	wceq	⊢ ( 𝑓 ‘ 𝑥 ) = 𝑥
22	18 21	wi	⊢ ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
23	22 10 12	wral	⊢ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
24	23 7 9	crab	⊢ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) }
25	3 6 24	cmpt	⊢ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
26	1 2 25	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
27	0 26	wceq	⊢ Dil = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )