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

Definition df-pautN 37007
Description: Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.)
Assertion
Ref Expression
df-pautN PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦)))})
Distinct variable group:   𝑓,𝑘,𝑥,𝑦

Detailed syntax breakdown of Definition df-pautN
StepHypRef Expression
1 cpautN 37003 . 2 class PAut
2 vk . . 3 setvar 𝑘
3 cvv 3492 . . 3 class V
42cv 1527 . . . . . . 7 class 𝑘
5 cpsubsp 36512 . . . . . . 7 class PSubSp
64, 5cfv 6348 . . . . . 6 class (PSubSp‘𝑘)
7 vf . . . . . . 7 setvar 𝑓
87cv 1527 . . . . . 6 class 𝑓
96, 6, 8wf1o 6347 . . . . 5 wff 𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘)
10 vx . . . . . . . . . 10 setvar 𝑥
1110cv 1527 . . . . . . . . 9 class 𝑥
12 vy . . . . . . . . . 10 setvar 𝑦
1312cv 1527 . . . . . . . . 9 class 𝑦
1411, 13wss 3933 . . . . . . . 8 wff 𝑥𝑦
1511, 8cfv 6348 . . . . . . . . 9 class (𝑓𝑥)
1613, 8cfv 6348 . . . . . . . . 9 class (𝑓𝑦)
1715, 16wss 3933 . . . . . . . 8 wff (𝑓𝑥) ⊆ (𝑓𝑦)
1814, 17wb 207 . . . . . . 7 wff (𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦))
1918, 12, 6wral 3135 . . . . . 6 wff 𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦))
2019, 10, 6wral 3135 . . . . 5 wff 𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦))
219, 20wa 396 . . . 4 wff (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦)))
2221, 7cab 2796 . . 3 class {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦)))}
232, 3, 22cmpt 5137 . 2 class (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦)))})
241, 23wceq 1528 1 wff PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥𝑦 ↔ (𝑓𝑥) ⊆ (𝑓𝑦)))})
Colors of variables: wff setvar class
This definition is referenced by:  pautsetN  37114
  Copyright terms: Public domain W3C validator