Definition df-lpolN 42117

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

Step	Hyp	Ref	Expression
1		clpoN 42116	. 2 class LPol
2		vw	. . 3 setvar 𝑤
3		cvv 3457	. . 3 class V
4	2	cv 1562	. . . . . . . 8 class 𝑤
5		cbs 17259	. . . . . . . 8 class Base
6	4, 5	cfv 6525	. . . . . . 7 class (Base‘𝑤)
7		vo	. . . . . . . 8 setvar 𝑜
8	7	cv 1562	. . . . . . 7 class 𝑜
9	6, 8	cfv 6525	. . . . . 6 class (𝑜‘(Base‘𝑤))
10		c0g 17482	. . . . . . . 8 class 0g
11	4, 10	cfv 6525	. . . . . . 7 class (0g‘𝑤)
12	11	csn 4585	. . . . . 6 class {(0g‘𝑤)}
13	9, 12	wceq 1563	. . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)}
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1562	. . . . . . . . . 10 class 𝑥
16	15, 6	wss 3907	. . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17		vy	. . . . . . . . . . 11 setvar 𝑦
18	17	cv 1562	. . . . . . . . . 10 class 𝑦
19	18, 6	wss 3907	. . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
20	15, 18	wss 3907	. . . . . . . . 9 wff 𝑥 ⊆ 𝑦
21	16, 19, 20	w3a 1101	. . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦)
22	18, 8	cfv 6525	. . . . . . . . 9 class (𝑜‘𝑦)
23	15, 8	cfv 6525	. . . . . . . . 9 class (𝑜‘𝑥)
24	22, 23	wss 3907	. . . . . . . 8 wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥)
25	21, 24	wi 4	. . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
26	25, 17	wal 1561	. . . . . 6 wff ∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
27	26, 14	wal 1561	. . . . 5 wff ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
28		clsh 39611	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 6525	. . . . . . . 8 class (LSHyp‘𝑤)
30	23, 29	wcel 2145	. . . . . . 7 wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤)
31	23, 8	cfv 6525	. . . . . . . 8 class (𝑜‘(𝑜‘𝑥))
32	31, 15	wceq 1563	. . . . . . 7 wff (𝑜‘(𝑜‘𝑥)) = 𝑥
33	30, 32	wa 400	. . . . . 6 wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
34		clsa 39610	. . . . . . 7 class LSAtoms
35	4, 34	cfv 6525	. . . . . 6 class (LSAtoms‘𝑤)
36	33, 14, 35	wral 3079	. . . . 5 wff ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
37	13, 27, 36	w3a 1101	. . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))
38		clss 21021	. . . . . 6 class LSubSp
39	4, 38	cfv 6525	. . . . 5 class (LSubSp‘𝑤)
40	6	cpw 4558	. . . . 5 class 𝒫 (Base‘𝑤)
41		cmap 8812	. . . . 5 class ↑m
42	39, 40, 41	co 7400	. . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
43	37, 7, 42	crab 3417	. . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}
44	2, 3, 43	cmpt 5186	. 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
45	1, 44	wceq 1563	1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})

This definition is referenced by:  lpolsetN  42118