df-lpolN

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)

		Ref	Expression
	Assertion	df-lpolN	$⊢ LPol = (w \in V ⟼ \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpoN	$class LPol$
1		vw	$setvar w$
2		cvv	$class V$
3		vo	$setvar o$
4		clss	$class LSubSp$
5	1	cv	$setvar w$
6	5 4	cfv	$class LSubSp (w)$
7		cmap	$class ↑_{𝑚}$
8		cbs	$class Base$
9	5 8	cfv	$class {Base}_{w}$
10	9	cpw	$class 𝒫 {Base}_{w}$
11	6 10 7	co	$class ({LSubSp (w)}^{𝒫 {Base}_{w}})$
12	3	cv	$setvar o$
13	9 12	cfv	$class o ({Base}_{w})$
14		c0g	$class 0_{𝑔}$
15	5 14	cfv	$class 0_{w}$
16	15	csn	$class \{0_{w}\}$
17	13 16	wceq	$wff o ({Base}_{w}) = \{0_{w}\}$
18		vx	$setvar x$
19		vy	$setvar y$
20	18	cv	$setvar x$
21	20 9	wss	$wff x \subseteq {Base}_{w}$
22	19	cv	$setvar y$
23	22 9	wss	$wff y \subseteq {Base}_{w}$
24	20 22	wss	$wff x \subseteq y$
25	21 23 24	w3a	$wff (x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y)$
26	22 12	cfv	$class o (y)$
27	20 12	cfv	$class o (x)$
28	26 27	wss	$wff o (y) \subseteq o (x)$
29	25 28	wi	$wff ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x))$
30	29 19	wal	$wff \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x))$
31	30 18	wal	$wff \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x))$
32		clsa	$class LSAtoms$
33	5 32	cfv	$class LSAtoms (w)$
34		clsh	$class LSHyp$
35	5 34	cfv	$class LSHyp (w)$
36	27 35	wcel	$wff o (x) \in LSHyp (w)$
37	27 12	cfv	$class o (o (x))$
38	37 20	wceq	$wff o (o (x)) = x$
39	36 38	wa	$wff (o (x) \in LSHyp (w) \land o (o (x)) = x)$
40	39 18 33	wral	$wff \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x)$
41	17 31 40	w3a	$wff (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))$
42	41 3 11	crab	$class \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\}$
43	1 2 42	cmpt	$class (w \in V ⟼ \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\})$
44	0 43	wceq	$wff LPol = (w \in V ⟼ \{o \in ({LSubSp (w)}^{𝒫 {Base}_{w}}) \| (o ({Base}_{w}) = \{0_{w}\} \land \forall x \forall y ((x \subseteq {Base}_{w} \land y \subseteq {Base}_{w} \land x \subseteq y) \to o (y) \subseteq o (x)) \land \forall x \in LSAtoms (w) (o (x) \in LSHyp (w) \land o (o (x)) = x))\})$

Metamath Proof Explorer

Definition df-lpolN

Detailed syntax breakdown