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 35689
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 35736.) (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 35688 . 2 class PCl
2 vk . . 3 setvar 𝑘
3 cvv 3349 . . 3 class V
4 vx . . . 4 setvar 𝑥
52cv 1629 . . . . . 6 class 𝑘
6 catm 35065 . . . . . 6 class Atoms
75, 6cfv 6031 . . . . 5 class (Atoms‘𝑘)
87cpw 4295 . . . 4 class 𝒫 (Atoms‘𝑘)
94cv 1629 . . . . . . 7 class 𝑥
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1629 . . . . . . 7 class 𝑦
129, 11wss 3721 . . . . . 6 wff 𝑥𝑦
13 cpsubsp 35297 . . . . . . 7 class PSubSp
145, 13cfv 6031 . . . . . 6 class (PSubSp‘𝑘)
1512, 10, 14crab 3064 . . . . 5 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}
1615cint 4609 . . . 4 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}
174, 8, 16cmpt 4861 . . 3 class (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦})
182, 3, 17cmpt 4861 . 2 class (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}))
191, 18wceq 1630 1 wff PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥𝑦}))
Colors of variables: wff setvar class
This definition is referenced by:  pclfvalN  35690
  Copyright terms: Public domain W3C validator