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 39091
 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‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
Distinct variable group:   𝑤,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-lpolN
StepHypRef Expression
1 clpoN 39090 . 2 class LPol
2 vw . . 3 setvar 𝑤
3 cvv 3409 . . 3 class V
42cv 1537 . . . . . . . 8 class 𝑤
5 cbs 16554 . . . . . . . 8 class Base
64, 5cfv 6340 . . . . . . 7 class (Base‘𝑤)
7 vo . . . . . . . 8 setvar 𝑜
87cv 1537 . . . . . . 7 class 𝑜
96, 8cfv 6340 . . . . . 6 class (𝑜‘(Base‘𝑤))
10 c0g 16784 . . . . . . . 8 class 0g
114, 10cfv 6340 . . . . . . 7 class (0g𝑤)
1211csn 4525 . . . . . 6 class {(0g𝑤)}
139, 12wceq 1538 . . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g𝑤)}
14 vx . . . . . . . . . . 11 setvar 𝑥
1514cv 1537 . . . . . . . . . 10 class 𝑥
1615, 6wss 3860 . . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17 vy . . . . . . . . . . 11 setvar 𝑦
1817cv 1537 . . . . . . . . . 10 class 𝑦
1918, 6wss 3860 . . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
2015, 18wss 3860 . . . . . . . . 9 wff 𝑥𝑦
2116, 19, 20w3a 1084 . . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦)
2218, 8cfv 6340 . . . . . . . . 9 class (𝑜𝑦)
2315, 8cfv 6340 . . . . . . . . 9 class (𝑜𝑥)
2422, 23wss 3860 . . . . . . . 8 wff (𝑜𝑦) ⊆ (𝑜𝑥)
2521, 24wi 4 . . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2625, 17wal 1536 . . . . . 6 wff 𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2726, 14wal 1536 . . . . 5 wff 𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
28 clsh 36585 . . . . . . . . 9 class LSHyp
294, 28cfv 6340 . . . . . . . 8 class (LSHyp‘𝑤)
3023, 29wcel 2111 . . . . . . 7 wff (𝑜𝑥) ∈ (LSHyp‘𝑤)
3123, 8cfv 6340 . . . . . . . 8 class (𝑜‘(𝑜𝑥))
3231, 15wceq 1538 . . . . . . 7 wff (𝑜‘(𝑜𝑥)) = 𝑥
3330, 32wa 399 . . . . . 6 wff ((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
34 clsa 36584 . . . . . . 7 class LSAtoms
354, 34cfv 6340 . . . . . 6 class (LSAtoms‘𝑤)
3633, 14, 35wral 3070 . . . . 5 wff 𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
3713, 27, 36w3a 1084 . . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))
38 clss 19784 . . . . . 6 class LSubSp
394, 38cfv 6340 . . . . 5 class (LSubSp‘𝑤)
406cpw 4497 . . . . 5 class 𝒫 (Base‘𝑤)
41 cmap 8422 . . . . 5 class m
4239, 40, 41co 7156 . . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
4337, 7, 42crab 3074 . . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))}
442, 3, 43cmpt 5116 . 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
451, 44wceq 1538 1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
 Colors of variables: wff setvar class This definition is referenced by:  lpolsetN  39092
 Copyright terms: Public domain W3C validator