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 40656
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 40655 . 2 class LPol
2 vw . . 3 setvar 𝑀
3 cvv 3473 . . 3 class V
42cv 1539 . . . . . . . 8 class 𝑀
5 cbs 17149 . . . . . . . 8 class Base
64, 5cfv 6543 . . . . . . 7 class (Baseβ€˜π‘€)
7 vo . . . . . . . 8 setvar π‘œ
87cv 1539 . . . . . . 7 class π‘œ
96, 8cfv 6543 . . . . . 6 class (π‘œβ€˜(Baseβ€˜π‘€))
10 c0g 17390 . . . . . . . 8 class 0g
114, 10cfv 6543 . . . . . . 7 class (0gβ€˜π‘€)
1211csn 4628 . . . . . 6 class {(0gβ€˜π‘€)}
139, 12wceq 1540 . . . . 5 wff (π‘œβ€˜(Baseβ€˜π‘€)) = {(0gβ€˜π‘€)}
14 vx . . . . . . . . . . 11 setvar π‘₯
1514cv 1539 . . . . . . . . . 10 class π‘₯
1615, 6wss 3948 . . . . . . . . 9 wff π‘₯ βŠ† (Baseβ€˜π‘€)
17 vy . . . . . . . . . . 11 setvar 𝑦
1817cv 1539 . . . . . . . . . 10 class 𝑦
1918, 6wss 3948 . . . . . . . . 9 wff 𝑦 βŠ† (Baseβ€˜π‘€)
2015, 18wss 3948 . . . . . . . . 9 wff π‘₯ βŠ† 𝑦
2116, 19, 20w3a 1086 . . . . . . . 8 wff (π‘₯ βŠ† (Baseβ€˜π‘€) ∧ 𝑦 βŠ† (Baseβ€˜π‘€) ∧ π‘₯ βŠ† 𝑦)
2218, 8cfv 6543 . . . . . . . . 9 class (π‘œβ€˜π‘¦)
2315, 8cfv 6543 . . . . . . . . 9 class (π‘œβ€˜π‘₯)
2422, 23wss 3948 . . . . . . . 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 38149 . . . . . . . . 9 class LSHyp
294, 28cfv 6543 . . . . . . . 8 class (LSHypβ€˜π‘€)
3023, 29wcel 2105 . . . . . . 7 wff (π‘œβ€˜π‘₯) ∈ (LSHypβ€˜π‘€)
3123, 8cfv 6543 . . . . . . . 8 class (π‘œβ€˜(π‘œβ€˜π‘₯))
3231, 15wceq 1540 . . . . . . 7 wff (π‘œβ€˜(π‘œβ€˜π‘₯)) = π‘₯
3330, 32wa 395 . . . . . 6 wff ((π‘œβ€˜π‘₯) ∈ (LSHypβ€˜π‘€) ∧ (π‘œβ€˜(π‘œβ€˜π‘₯)) = π‘₯)
34 clsa 38148 . . . . . . 7 class LSAtoms
354, 34cfv 6543 . . . . . 6 class (LSAtomsβ€˜π‘€)
3633, 14, 35wral 3060 . . . . 5 wff βˆ€π‘₯ ∈ (LSAtomsβ€˜π‘€)((π‘œβ€˜π‘₯) ∈ (LSHypβ€˜π‘€) ∧ (π‘œβ€˜(π‘œβ€˜π‘₯)) = π‘₯)
3713, 27, 36w3a 1086 . . . 4 wff ((π‘œβ€˜(Baseβ€˜π‘€)) = {(0gβ€˜π‘€)} ∧ βˆ€π‘₯βˆ€π‘¦((π‘₯ βŠ† (Baseβ€˜π‘€) ∧ 𝑦 βŠ† (Baseβ€˜π‘€) ∧ π‘₯ βŠ† 𝑦) β†’ (π‘œβ€˜π‘¦) βŠ† (π‘œβ€˜π‘₯)) ∧ βˆ€π‘₯ ∈ (LSAtomsβ€˜π‘€)((π‘œβ€˜π‘₯) ∈ (LSHypβ€˜π‘€) ∧ (π‘œβ€˜(π‘œβ€˜π‘₯)) = π‘₯))
38 clss 20687 . . . . . 6 class LSubSp
394, 38cfv 6543 . . . . 5 class (LSubSpβ€˜π‘€)
406cpw 4602 . . . . 5 class 𝒫 (Baseβ€˜π‘€)
41 cmap 8823 . . . . 5 class ↑m
4239, 40, 41co 7412 . . . 4 class ((LSubSpβ€˜π‘€) ↑m 𝒫 (Baseβ€˜π‘€))
4337, 7, 42crab 3431 . . 3 class {π‘œ ∈ ((LSubSpβ€˜π‘€) ↑m 𝒫 (Baseβ€˜π‘€)) ∣ ((π‘œβ€˜(Baseβ€˜π‘€)) = {(0gβ€˜π‘€)} ∧ βˆ€π‘₯βˆ€π‘¦((π‘₯ βŠ† (Baseβ€˜π‘€) ∧ 𝑦 βŠ† (Baseβ€˜π‘€) ∧ π‘₯ βŠ† 𝑦) β†’ (π‘œβ€˜π‘¦) βŠ† (π‘œβ€˜π‘₯)) ∧ βˆ€π‘₯ ∈ (LSAtomsβ€˜π‘€)((π‘œβ€˜π‘₯) ∈ (LSHypβ€˜π‘€) ∧ (π‘œβ€˜(π‘œβ€˜π‘₯)) = π‘₯))}
442, 3, 43cmpt 5231 . 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  40657
  Copyright terms: Public domain W3C validator