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 35587
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 35586 . 2 class LPol
2 vw . . 3 setvar 𝑤
3 cvv 3168 . . 3 class V
42cv 1473 . . . . . . . 8 class 𝑤
5 cbs 15637 . . . . . . . 8 class Base
64, 5cfv 5786 . . . . . . 7 class (Base‘𝑤)
7 vo . . . . . . . 8 setvar 𝑜
87cv 1473 . . . . . . 7 class 𝑜
96, 8cfv 5786 . . . . . 6 class (𝑜‘(Base‘𝑤))
10 c0g 15865 . . . . . . . 8 class 0g
114, 10cfv 5786 . . . . . . 7 class (0g𝑤)
1211csn 4120 . . . . . 6 class {(0g𝑤)}
139, 12wceq 1474 . . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g𝑤)}
14 vx . . . . . . . . . . 11 setvar 𝑥
1514cv 1473 . . . . . . . . . 10 class 𝑥
1615, 6wss 3535 . . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17 vy . . . . . . . . . . 11 setvar 𝑦
1817cv 1473 . . . . . . . . . 10 class 𝑦
1918, 6wss 3535 . . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
2015, 18wss 3535 . . . . . . . . 9 wff 𝑥𝑦
2116, 19, 20w3a 1030 . . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦)
2218, 8cfv 5786 . . . . . . . . 9 class (𝑜𝑦)
2315, 8cfv 5786 . . . . . . . . 9 class (𝑜𝑥)
2422, 23wss 3535 . . . . . . . 8 wff (𝑜𝑦) ⊆ (𝑜𝑥)
2521, 24wi 4 . . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2625, 17wal 1472 . . . . . 6 wff 𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
2726, 14wal 1472 . . . . 5 wff 𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥))
28 clsh 33079 . . . . . . . . 9 class LSHyp
294, 28cfv 5786 . . . . . . . 8 class (LSHyp‘𝑤)
3023, 29wcel 1975 . . . . . . 7 wff (𝑜𝑥) ∈ (LSHyp‘𝑤)
3123, 8cfv 5786 . . . . . . . 8 class (𝑜‘(𝑜𝑥))
3231, 15wceq 1474 . . . . . . 7 wff (𝑜‘(𝑜𝑥)) = 𝑥
3330, 32wa 382 . . . . . 6 wff ((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
34 clsa 33078 . . . . . . 7 class LSAtoms
354, 34cfv 5786 . . . . . 6 class (LSAtoms‘𝑤)
3633, 14, 35wral 2891 . . . . 5 wff 𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥)
3713, 27, 36w3a 1030 . . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))
38 clss 18695 . . . . . 6 class LSubSp
394, 38cfv 5786 . . . . 5 class (LSubSp‘𝑤)
406cpw 4103 . . . . 5 class 𝒫 (Base‘𝑤)
41 cmap 7717 . . . . 5 class 𝑚
4239, 40, 41co 6523 . . . 4 class ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤))
4337, 7, 42crab 2895 . . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))}
442, 3, 43cmpt 4633 . 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
451, 44wceq 1474 1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑𝑚 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g𝑤)} ∧ ∀𝑥𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥𝑦) → (𝑜𝑦) ⊆ (𝑜𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜𝑥)) = 𝑥))})
Colors of variables: wff setvar class
This definition is referenced by:  lpolsetN  35588
  Copyright terms: Public domain W3C validator