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

Definition df-lpolN 35788
Description: Define the set of all polarities of a left module or left vector space. A polarity is a kind of complementation operation on a subspace. The double polarity of a subspace is a closure operation. Based on Definition 3.2 of [Holland95] p. 214 for projective geometry polarities. For convenience, we open up the domain to include all vector subsets and not just subspaces, but any more restricted polarity can be converted to this one by taking the span of its argument. (Contributed by NM, 24-Nov-2014.)
Assertion
Ref Expression
df-lpolN LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
Distinct variable group:   𝑤,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-lpolN
StepHypRef Expression
1 clpoN 35787 . 2 class LPol
2 vw . . 3 setvar 𝑤
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . . . 8 class 𝑤
5 cbs 15695 . . . . . . . 8 class Base
64, 5cfv 5804 . . . . . . 7 class (Base‘𝑤)
7 vo . . . . . . . 8 setvar 𝑜
87cv 1474 . . . . . . 7 class 𝑜
96, 8cfv 5804 . . . . . 6 class (𝑜‘(Base‘𝑤))
10 c0g 15923 . . . . . . . 8 class 0g
114, 10cfv 5804 . . . . . . 7 class (0g𝑤)
1211csn 4125 . . . . . 6 class {(0g𝑤)}
139, 12wceq 1475 . . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g𝑤)}
14 vx . . . . . . . . . . 11 setvar 𝑥
1514cv 1474 . . . . . . . . . 10 class 𝑥
1615, 6wss 3540 . . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17 vy . . . . . . . . . . 11 setvar 𝑦
1817cv 1474 . . . . . . . . . 10 class 𝑦
1918, 6wss 3540 . . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
2015, 18wss 3540 . . . . . . . . 9 wff 𝑥𝑦
2116, 19, 20w3a 1031 . . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦)
2218, 8cfv 5804 . . . . . . . . 9 class (𝑜𝑦)
2315, 8cfv 5804 . . . . . . . . 9 class (𝑜𝑥)
2422, 23wss 3540 . . . . . . . 8 wff (𝑜𝑦) ⊆ (𝑜𝑥)
2521, 24wi 4 . . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2625, 17wal 1473 . . . . . 6 wff 𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2726, 14wal 1473 . . . . 5 wff 𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
28 clsh 33280 . . . . . . . . 9 class LSHyp
294, 28cfv 5804 . . . . . . . 8 class (LSHyp‘𝑤)
3023, 29wcel 1977 . . . . . . 7 wff (𝑜𝑥) ∈ (LSHyp‘𝑤)
3123, 8cfv 5804 . . . . . . . 8 class (𝑜‘(𝑜𝑥))
3231, 15wceq 1475 . . . . . . 7 wff (𝑜‘(𝑜𝑥)) = 𝑥
3330, 32wa 383 . . . . . 6 wff ((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
34 clsa 33279 . . . . . . 7 class LSAtoms
354, 34cfv 5804 . . . . . 6 class (LSAtoms‘𝑤)
3633, 14, 35wral 2896 . . . . 5 wff 𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
3713, 27, 36w3a 1031 . . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))
38 clss 18753 . . . . . 6 class LSubSp
394, 38cfv 5804 . . . . 5 class (LSubSp‘𝑤)
406cpw 4108 . . . . 5 class 𝒫 (Base‘𝑤)
41 cmap 7744 . . . . 5 class 𝑚
4239, 40, 41co 6549 . . . 4 class ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤))
4337, 7, 42crab 2900 . . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))}
442, 3, 43cmpt 4643 . 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
451, 44wceq 1475 1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
Colors of variables: wff setvar class
This definition is referenced by:  lpolsetN  35789
  Copyright terms: Public domain W3C validator