Definition df-lpolN 41464

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 41463	. 2 class LPol
2		vw	. . 3 setvar 𝑤
3		cvv 3478	. . 3 class V
4	2	cv 1536	. . . . . . . 8 class 𝑤
5		cbs 17245	. . . . . . . 8 class Base
6	4, 5	cfv 6563	. . . . . . 7 class (Base‘𝑤)
7		vo	. . . . . . . 8 setvar 𝑜
8	7	cv 1536	. . . . . . 7 class 𝑜
9	6, 8	cfv 6563	. . . . . 6 class (𝑜‘(Base‘𝑤))
10		c0g 17486	. . . . . . . 8 class 0g
11	4, 10	cfv 6563	. . . . . . 7 class (0g‘𝑤)
12	11	csn 4631	. . . . . 6 class {(0g‘𝑤)}
13	9, 12	wceq 1537	. . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)}
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1536	. . . . . . . . . 10 class 𝑥
16	15, 6	wss 3963	. . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17		vy	. . . . . . . . . . 11 setvar 𝑦
18	17	cv 1536	. . . . . . . . . 10 class 𝑦
19	18, 6	wss 3963	. . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
20	15, 18	wss 3963	. . . . . . . . 9 wff 𝑥 ⊆ 𝑦
21	16, 19, 20	w3a 1086	. . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦)
22	18, 8	cfv 6563	. . . . . . . . 9 class (𝑜‘𝑦)
23	15, 8	cfv 6563	. . . . . . . . 9 class (𝑜‘𝑥)
24	22, 23	wss 3963	. . . . . . . 8 wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥)
25	21, 24	wi 4	. . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
26	25, 17	wal 1535	. . . . . 6 wff ∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
27	26, 14	wal 1535	. . . . 5 wff ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
28		clsh 38957	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 6563	. . . . . . . 8 class (LSHyp‘𝑤)
30	23, 29	wcel 2106	. . . . . . 7 wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤)
31	23, 8	cfv 6563	. . . . . . . 8 class (𝑜‘(𝑜‘𝑥))
32	31, 15	wceq 1537	. . . . . . 7 wff (𝑜‘(𝑜‘𝑥)) = 𝑥
33	30, 32	wa 395	. . . . . 6 wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
34		clsa 38956	. . . . . . 7 class LSAtoms
35	4, 34	cfv 6563	. . . . . 6 class (LSAtoms‘𝑤)
36	33, 14, 35	wral 3059	. . . . 5 wff ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
37	13, 27, 36	w3a 1086	. . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))
38		clss 20947	. . . . . 6 class LSubSp
39	4, 38	cfv 6563	. . . . 5 class (LSubSp‘𝑤)
40	6	cpw 4605	. . . . 5 class 𝒫 (Base‘𝑤)
41		cmap 8865	. . . . 5 class ↑m
42	39, 40, 41	co 7431	. . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
43	37, 7, 42	crab 3433	. . 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 1537	1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})

This definition is referenced by:  lpolsetN  41465