Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dilN Structured version   Visualization version   GIF version

Definition df-dilN 34410
 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
StepHypRef Expression
1 cdilN 34406 . 2 class Dil
2 vk . . 3 setvar 𝑘
3 cvv 3173 . . 3 class V
4 vd . . . 4 setvar 𝑑
52cv 1474 . . . . 5 class 𝑘
6 catm 33568 . . . . 5 class Atoms
75, 6cfv 5804 . . . 4 class (Atoms‘𝑘)
8 vx . . . . . . . . 9 setvar 𝑥
98cv 1474 . . . . . . . 8 class 𝑥
104cv 1474 . . . . . . . . 9 class 𝑑
11 cwpointsN 34290 . . . . . . . . . 10 class WAtoms
125, 11cfv 5804 . . . . . . . . 9 class (WAtoms‘𝑘)
1310, 12cfv 5804 . . . . . . . 8 class ((WAtoms‘𝑘)‘𝑑)
149, 13wss 3540 . . . . . . 7 wff 𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑)
15 vf . . . . . . . . . 10 setvar 𝑓
1615cv 1474 . . . . . . . . 9 class 𝑓
179, 16cfv 5804 . . . . . . . 8 class (𝑓𝑥)
1817, 9wceq 1475 . . . . . . 7 wff (𝑓𝑥) = 𝑥
1914, 18wi 4 . . . . . 6 wff (𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)
20 cpsubsp 33800 . . . . . . 7 class PSubSp
215, 20cfv 5804 . . . . . 6 class (PSubSp‘𝑘)
2219, 8, 21wral 2896 . . . . 5 wff 𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)
23 cpautN 34291 . . . . . 6 class PAut
245, 23cfv 5804 . . . . 5 class (PAut‘𝑘)
2522, 15, 24crab 2900 . . . 4 class {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)}
264, 7, 25cmpt 4643 . . 3 class (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)})
272, 3, 26cmpt 4643 . 2 class (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)}))
281, 27wceq 1475 1 wff Dil = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓𝑥) = 𝑥)}))
 Colors of variables: wff setvar class This definition is referenced by:  dilfsetN  34457
 Copyright terms: Public domain W3C validator