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 41483
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 41482 . 2 class LPol
2 vw . . 3 setvar 𝑤
3 cvv 3480 . . 3 class V
42cv 1539 . . . . . . . 8 class 𝑤
5 cbs 17247 . . . . . . . 8 class Base
64, 5cfv 6561 . . . . . . 7 class (Base‘𝑤)
7 vo . . . . . . . 8 setvar 𝑜
87cv 1539 . . . . . . 7 class 𝑜
96, 8cfv 6561 . . . . . 6 class (𝑜‘(Base‘𝑤))
10 c0g 17484 . . . . . . . 8 class 0g
114, 10cfv 6561 . . . . . . 7 class (0g𝑤)
1211csn 4626 . . . . . 6 class {(0g𝑤)}
139, 12wceq 1540 . . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g𝑤)}
14 vx . . . . . . . . . . 11 setvar 𝑥
1514cv 1539 . . . . . . . . . 10 class 𝑥
1615, 6wss 3951 . . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17 vy . . . . . . . . . . 11 setvar 𝑦
1817cv 1539 . . . . . . . . . 10 class 𝑦
1918, 6wss 3951 . . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
2015, 18wss 3951 . . . . . . . . 9 wff 𝑥𝑦
2116, 19, 20w3a 1087 . . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦)
2218, 8cfv 6561 . . . . . . . . 9 class (𝑜𝑦)
2315, 8cfv 6561 . . . . . . . . 9 class (𝑜𝑥)
2422, 23wss 3951 . . . . . . . 8 wff (𝑜𝑦) ⊆ (𝑜𝑥)
2521, 24wi 4 . . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2625, 17wal 1538 . . . . . 6 wff 𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2726, 14wal 1538 . . . . 5 wff 𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
28 clsh 38976 . . . . . . . . 9 class LSHyp
294, 28cfv 6561 . . . . . . . 8 class (LSHyp‘𝑤)
3023, 29wcel 2108 . . . . . . 7 wff (𝑜𝑥) ∈ (LSHyp‘𝑤)
3123, 8cfv 6561 . . . . . . . 8 class (𝑜‘(𝑜𝑥))
3231, 15wceq 1540 . . . . . . 7 wff (𝑜‘(𝑜𝑥)) = 𝑥
3330, 32wa 395 . . . . . 6 wff ((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
34 clsa 38975 . . . . . . 7 class LSAtoms
354, 34cfv 6561 . . . . . 6 class (LSAtoms‘𝑤)
3633, 14, 35wral 3061 . . . . 5 wff 𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
3713, 27, 36w3a 1087 . . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))
38 clss 20929 . . . . . 6 class LSubSp
394, 38cfv 6561 . . . . 5 class (LSubSp‘𝑤)
406cpw 4600 . . . . 5 class 𝒫 (Base‘𝑤)
41 cmap 8866 . . . . 5 class m
4239, 40, 41co 7431 . . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
4337, 7, 42crab 3436 . . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))}
442, 3, 43cmpt 5225 . 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
451, 44wceq 1540 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  41484
  Copyright terms: Public domain W3C validator