Definition df-dilN 40130

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

Distinct variable group:   𝑘,𝑑,𝑓,𝑥

Detailed syntax breakdown of Definition df-dilN

Step	Hyp	Ref	Expression
1		cdilN 40126	. 2 class Dil
2		vk	. . 3 setvar 𝑘
3		cvv 3464	. . 3 class V
4		vd	. . . 4 setvar 𝑑
5	2	cv 1539	. . . . 5 class 𝑘
6		catm 39286	. . . . 5 class Atoms
7	5, 6	cfv 6536	. . . 4 class (Atoms‘𝑘)
8		vx	. . . . . . . . 9 setvar 𝑥
9	8	cv 1539	. . . . . . . 8 class 𝑥
10	4	cv 1539	. . . . . . . . 9 class 𝑑
11		cwpointsN 40010	. . . . . . . . . 10 class WAtoms
12	5, 11	cfv 6536	. . . . . . . . 9 class (WAtoms‘𝑘)
13	10, 12	cfv 6536	. . . . . . . 8 class ((WAtoms‘𝑘)‘𝑑)
14	9, 13	wss 3931	. . . . . . 7 wff 𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑)
15		vf	. . . . . . . . . 10 setvar 𝑓
16	15	cv 1539	. . . . . . . . 9 class 𝑓
17	9, 16	cfv 6536	. . . . . . . 8 class (𝑓‘𝑥)
18	17, 9	wceq 1540	. . . . . . 7 wff (𝑓‘𝑥) = 𝑥
19	14, 18	wi 4	. . . . . 6 wff (𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)
20		cpsubsp 39520	. . . . . . 7 class PSubSp
21	5, 20	cfv 6536	. . . . . 6 class (PSubSp‘𝑘)
22	19, 8, 21	wral 3052	. . . . 5 wff ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)
23		cpautN 40011	. . . . . 6 class PAut
24	5, 23	cfv 6536	. . . . 5 class (PAut‘𝑘)
25	22, 15, 24	crab 3420	. . . 4 class {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}
26	4, 7, 25	cmpt 5206	. . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)})
27	2, 3, 26	cmpt 5206	. 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}))
28	1, 27	wceq 1540	1 wff Dil = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}))

This definition is referenced by:  dilfsetN  40176