Definition df-lpolN 40982

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 40981	. 2 class LPol
2		vw	. . 3 setvar 𝑤
3		cvv 3463	. . 3 class V
4	2	cv 1532	. . . . . . . 8 class 𝑤
5		cbs 17177	. . . . . . . 8 class Base
6	4, 5	cfv 6541	. . . . . . 7 class (Base‘𝑤)
7		vo	. . . . . . . 8 setvar 𝑜
8	7	cv 1532	. . . . . . 7 class 𝑜
9	6, 8	cfv 6541	. . . . . 6 class (𝑜‘(Base‘𝑤))
10		c0g 17418	. . . . . . . 8 class 0g
11	4, 10	cfv 6541	. . . . . . 7 class (0g‘𝑤)
12	11	csn 4622	. . . . . 6 class {(0g‘𝑤)}
13	9, 12	wceq 1533	. . . . 5 wff (𝑜‘(Base‘𝑤)) = {(0g‘𝑤)}
14		vx	. . . . . . . . . . 11 setvar 𝑥
15	14	cv 1532	. . . . . . . . . 10 class 𝑥
16	15, 6	wss 3939	. . . . . . . . 9 wff 𝑥 ⊆ (Base‘𝑤)
17		vy	. . . . . . . . . . 11 setvar 𝑦
18	17	cv 1532	. . . . . . . . . 10 class 𝑦
19	18, 6	wss 3939	. . . . . . . . 9 wff 𝑦 ⊆ (Base‘𝑤)
20	15, 18	wss 3939	. . . . . . . . 9 wff 𝑥 ⊆ 𝑦
21	16, 19, 20	w3a 1084	. . . . . . . 8 wff (𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦)
22	18, 8	cfv 6541	. . . . . . . . 9 class (𝑜‘𝑦)
23	15, 8	cfv 6541	. . . . . . . . 9 class (𝑜‘𝑥)
24	22, 23	wss 3939	. . . . . . . 8 wff (𝑜‘𝑦) ⊆ (𝑜‘𝑥)
25	21, 24	wi 4	. . . . . . 7 wff ((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
26	25, 17	wal 1531	. . . . . 6 wff ∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
27	26, 14	wal 1531	. . . . 5 wff ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥))
28		clsh 38475	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 6541	. . . . . . . 8 class (LSHyp‘𝑤)
30	23, 29	wcel 2098	. . . . . . 7 wff (𝑜‘𝑥) ∈ (LSHyp‘𝑤)
31	23, 8	cfv 6541	. . . . . . . 8 class (𝑜‘(𝑜‘𝑥))
32	31, 15	wceq 1533	. . . . . . 7 wff (𝑜‘(𝑜‘𝑥)) = 𝑥
33	30, 32	wa 394	. . . . . 6 wff ((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
34		clsa 38474	. . . . . . 7 class LSAtoms
35	4, 34	cfv 6541	. . . . . 6 class (LSAtoms‘𝑤)
36	33, 14, 35	wral 3051	. . . . 5 wff ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥)
37	13, 27, 36	w3a 1084	. . . 4 wff ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))
38		clss 20817	. . . . . 6 class LSubSp
39	4, 38	cfv 6541	. . . . 5 class (LSubSp‘𝑤)
40	6	cpw 4596	. . . . 5 class 𝒫 (Base‘𝑤)
41		cmap 8841	. . . . 5 class ↑m
42	39, 40, 41	co 7414	. . . 4 class ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤))
43	37, 7, 42	crab 3419	. . 3 class {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))}
44	2, 3, 43	cmpt 5224	. 2 class (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})
45	1, 44	wceq 1533	1 wff LPol = (𝑤 ∈ V ↦ {𝑜 ∈ ((LSubSp‘𝑤) ↑m 𝒫 (Base‘𝑤)) ∣ ((𝑜‘(Base‘𝑤)) = {(0g‘𝑤)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ (Base‘𝑤) ∧ 𝑦 ⊆ (Base‘𝑤) ∧ 𝑥 ⊆ 𝑦) → (𝑜‘𝑦) ⊆ (𝑜‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑤)((𝑜‘𝑥) ∈ (LSHyp‘𝑤) ∧ (𝑜‘(𝑜‘𝑥)) = 𝑥))})

This definition is referenced by:  lpolsetN  40983

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »