Definition df-lpolN 40948

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 40947	. 2 class LPol
2		vw	. . 3 setvar 𝑤
3		cvv 3470	. . 3 class V
4	2	cv 1533	. . . . . . . 8 class 𝑤
5		cbs 17173	. . . . . . . 8 class Base
6	4, 5	cfv 6542	. . . . . . 7 class (Base‘𝑤)
7		vo	. . . . . . . 8 setvar 𝑜
8	7	cv 1533	. . . . . . 7 class 𝑜
9	6, 8	cfv 6542	. . . . . 6 class (𝑜‘(Base‘𝑤))
10		c0g 17414	. . . . . . . 8 class 0g
11	4, 10	cfv 6542	. . . . . . 7 class (0g‘𝑤)
12	11	csn 4624	. . . . . 6 class {(0g‘𝑤)}
13	9, 12	wceq 1534	. . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)}
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1533	. . . . . . . . . 10 class 𝑥
16	15, 6	wss 3945	. . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17		vy	. . . . . . . . . . 11 setvar 𝑦
18	17	cv 1533	. . . . . . . . . 10 class 𝑦
19	18, 6	wss 3945	. . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
20	15, 18	wss 3945	. . . . . . . . 9 wff 𝑥 ⊆ 𝑦
21	16, 19, 20	w3a 1085	. . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦)
22	18, 8	cfv 6542	. . . . . . . . 9 class (𝑜‘𝑦)
23	15, 8	cfv 6542	. . . . . . . . 9 class (𝑜‘𝑥)
24	22, 23	wss 3945	. . . . . . . 8 wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥)
25	21, 24	wi 4	. . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
26	25, 17	wal 1532	. . . . . 6 wff ∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
27	26, 14	wal 1532	. . . . 5 wff ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
28		clsh 38441	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 6542	. . . . . . . 8 class (LSHyp‘𝑤)
30	23, 29	wcel 2099	. . . . . . 7 wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤)
31	23, 8	cfv 6542	. . . . . . . 8 class (𝑜‘(𝑜‘𝑥))
32	31, 15	wceq 1534	. . . . . . 7 wff (𝑜‘(𝑜‘𝑥)) = 𝑥
33	30, 32	wa 395	. . . . . 6 wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
34		clsa 38440	. . . . . . 7 class LSAtoms
35	4, 34	cfv 6542	. . . . . 6 class (LSAtoms‘𝑤)
36	33, 14, 35	wral 3057	. . . . 5 wff ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
37	13, 27, 36	w3a 1085	. . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))
38		clss 20808	. . . . . 6 class LSubSp
39	4, 38	cfv 6542	. . . . 5 class (LSubSp‘𝑤)
40	6	cpw 4598	. . . . 5 class 𝒫 (Base‘𝑤)
41		cmap 8838	. . . . 5 class ↑m
42	39, 40, 41	co 7414	. . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
43	37, 7, 42	crab 3428	. . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}
44	2, 3, 43	cmpt 5225	. 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
45	1, 44	wceq 1534	1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})

This definition is referenced by:  lpolsetN  40949