Definition df-lpolN 36770

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 = ( w e. _V |-> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } )

Distinct variable group:   w, o, x, y

Detailed syntax breakdown of Definition df-lpolN

Step	Hyp	Ref	Expression
1		clpoN 36769	. 2 class LPol
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . . . . 8 class w
5		cbs 15857	. . . . . . . 8 class Base
6	4, 5	cfv 5888	. . . . . . 7 class ( Base ` w )
7		vo	. . . . . . . 8 setvar o
8	7	cv 1482	. . . . . . 7 class o
9	6, 8	cfv 5888	. . . . . 6 class ( o ` ( Base ` w ) )
10		c0g 16100	. . . . . . . 8 class 0g
11	4, 10	cfv 5888	. . . . . . 7 class ( 0g ` w )
12	11	csn 4177	. . . . . 6 class { ( 0g ` w ) }
13	9, 12	wceq 1483	. . . . 5 wff ( o ` ( Base ` w ) ) = { ( 0g ` w ) }
14		vx	. . . . . . . . . . 11 setvar x
15	14	cv 1482	. . . . . . . . . 10 class x
16	15, 6	wss 3574	. . . . . . . . 9 wff x C_ ( Base ` w )
17		vy	. . . . . . . . . . 11 setvar y
18	17	cv 1482	. . . . . . . . . 10 class y
19	18, 6	wss 3574	. . . . . . . . 9 wff y C_ ( Base ` w )
20	15, 18	wss 3574	. . . . . . . . 9 wff x C_ y
21	16, 19, 20	w3a 1037	. . . . . . . 8 wff ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y )
22	18, 8	cfv 5888	. . . . . . . . 9 class ( o ` y )
23	15, 8	cfv 5888	. . . . . . . . 9 class ( o ` x )
24	22, 23	wss 3574	. . . . . . . 8 wff ( o ` y ) C_ ( o ` x )
25	21, 24	wi 4	. . . . . . 7 wff ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) )
26	25, 17	wal 1481	. . . . . 6 wff A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) )
27	26, 14	wal 1481	. . . . 5 wff A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) )
28		clsh 34262	. . . . . . . . 9 class LSHyp
29	4, 28	cfv 5888	. . . . . . . 8 class (LSHyp ` w )
30	23, 29	wcel 1990	. . . . . . 7 wff ( o ` x ) e. (LSHyp ` w )
31	23, 8	cfv 5888	. . . . . . . 8 class ( o ` ( o ` x ) )
32	31, 15	wceq 1483	. . . . . . 7 wff ( o ` ( o ` x ) ) = x
33	30, 32	wa 384	. . . . . 6 wff ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x )
34		clsa 34261	. . . . . . 7 class LSAtoms
35	4, 34	cfv 5888	. . . . . 6 class (LSAtoms ` w )
36	33, 14, 35	wral 2912	. . . . 5 wff A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x )
37	13, 27, 36	w3a 1037	. . . 4 wff ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) )
38		clss 18932	. . . . . 6 class LSubSp
39	4, 38	cfv 5888	. . . . 5 class ( LSubSp ` w )
40	6	cpw 4158	. . . . 5 class ~P ( Base ` w )
41		cmap 7857	. . . . 5 class ^m
42	39, 40, 41	co 6650	. . . 4 class ( ( LSubSp ` w ) ^m ~P ( Base ` w ) )
43	37, 7, 42	crab 2916	. . 3 class { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) }
44	2, 3, 43	cmpt 4729	. 2 class ( w e. _V |-> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } )
45	1, 44	wceq 1483	1 wff LPol = ( w e. _V |-> { o e. ( ( LSubSp ` w ) ^m ~P ( Base ` w ) ) | ( ( o ` ( Base ` w ) ) = { ( 0g ` w ) } /\ A. x A. y ( ( x C_ ( Base ` w ) /\ y C_ ( Base ` w ) /\ x C_ y ) -> ( o ` y ) C_ ( o ` x ) ) /\ A. x e. (LSAtoms ` w ) ( ( o ` x ) e. (LSHyp ` w ) /\ ( o ` ( o ` x ) ) = x ) ) } )

This definition is referenced by:  lpolsetN  36771