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

Definition df-pclN 35492
Description: Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces PSubCl of df-psubclN 35539.) (Contributed by NM, 7-Sep-2013.)
Assertion
Ref Expression
df-pclN PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}))
Distinct variable group:   𝑥,𝑘,𝑦

Detailed syntax breakdown of Definition df-pclN
StepHypRef Expression
1 cpclN 35491 . 2 class PCl
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1522 . . . . . 6 class 𝑘
6 catm 34868 . . . . . 6 class Atoms
75, 6cfv 5926 . . . . 5 class (Atoms‘𝑘)
87cpw 4191 . . . 4 class 𝒫 (Atoms‘𝑘)
94cv 1522 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1522 . . . . . . 7 class 𝑦
129, 11wss 3607 . . . . . 6 wff 𝑥𝑦
13 cpsubsp 35100 . . . . . . 7 class PSubSp
145, 13cfv 5926 . . . . . 6 class (PSubSp‘𝑘)
1512, 10, 14crab 2945 . . . . 5 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}
1615cint 4507 . . . 4 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}
174, 8, 16cmpt 4762 . . 3 class (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦})
182, 3, 17cmpt 4762 . 2 class (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}))
191, 18wceq 1523 1 wff PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}))
Colors of variables: wff setvar class
This definition is referenced by:  pclfvalN  35493
  Copyright terms: Public domain W3C validator