Definition df-lpolN 40438

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 40437	. 2 class LPol
2		vw	. . 3 setvar 𝑤
3		cvv 3474	. . 3 class V
4	2	cv 1540	. . . . . . . 8 class 𝑤
5		cbs 17146	. . . . . . . 8 class Base
6	4, 5	cfv 6543	. . . . . . 7 class (Base‘𝑤)
7		vo	. . . . . . . 8 setvar 𝑜
8	7	cv 1540	. . . . . . 7 class 𝑜
9	6, 8	cfv 6543	. . . . . 6 class (𝑜‘(Base‘𝑤))
10		c0g 17387	. . . . . . . 8 class 0g
11	4, 10	cfv 6543	. . . . . . 7 class (0g‘𝑤)
12	11	csn 4628	. . . . . 6 class {(0g‘𝑤)}
13	9, 12	wceq 1541	. . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)}
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1540	. . . . . . . . . 10 class 𝑥
16	15, 6	wss 3948	. . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17		vy	. . . . . . . . . . 11 setvar 𝑦
18	17	cv 1540	. . . . . . . . . 10 class 𝑦
19	18, 6	wss 3948	. . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
20	15, 18	wss 3948	. . . . . . . . 9 wff 𝑥 ⊆ 𝑦
21	16, 19, 20	w3a 1087	. . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦)
22	18, 8	cfv 6543	. . . . . . . . 9 class (𝑜‘𝑦)
23	15, 8	cfv 6543	. . . . . . . . 9 class (𝑜‘𝑥)
24	22, 23	wss 3948	. . . . . . . 8 wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥)
25	21, 24	wi 4	. . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
26	25, 17	wal 1539	. . . . . 6 wff ∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
27	26, 14	wal 1539	. . . . 5 wff ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
28		clsh 37931	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 6543	. . . . . . . 8 class (LSHyp‘𝑤)
30	23, 29	wcel 2106	. . . . . . 7 wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤)
31	23, 8	cfv 6543	. . . . . . . 8 class (𝑜‘(𝑜‘𝑥))
32	31, 15	wceq 1541	. . . . . . 7 wff (𝑜‘(𝑜‘𝑥)) = 𝑥
33	30, 32	wa 396	. . . . . 6 wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
34		clsa 37930	. . . . . . 7 class LSAtoms
35	4, 34	cfv 6543	. . . . . 6 class (LSAtoms‘𝑤)
36	33, 14, 35	wral 3061	. . . . 5 wff ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
37	13, 27, 36	w3a 1087	. . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))
38		clss 20547	. . . . . 6 class LSubSp
39	4, 38	cfv 6543	. . . . 5 class (LSubSp‘𝑤)
40	6	cpw 4602	. . . . 5 class 𝒫 (Base‘𝑤)
41		cmap 8822	. . . . 5 class ↑m
42	39, 40, 41	co 7411	. . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
43	37, 7, 42	crab 3432	. . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}
44	2, 3, 43	cmpt 5231	. 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
45	1, 44	wceq 1541	1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})

This definition is referenced by:  lpolsetN  40439