Definition df-polarityN

Description: Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in Holland95 p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with Atomsl ensures it is defined when m = (/) . (Contributed by NM, 23-Oct-2011)

	Ref	Expression
Assertion	df-polarityN	|- _|_P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpolN	|- _|_P
1		vl	|- l
2		cvv	|- _V
3		vm	|- m
4		catm	|- Atoms
5	1	cv	|- l
6	5 4	cfv	|- ( Atoms ` l )
7	6	cpw	|- ~P ( Atoms ` l )
8		vp	|- p
9	3	cv	|- m
10		cpmap	|- pmap
11	5 10	cfv	|- ( pmap ` l )
12		coc	|- oc
13	5 12	cfv	|- ( oc ` l )
14	8	cv	|- p
15	14 13	cfv	|- ( ( oc ` l ) ` p )
16	15 11	cfv	|- ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) )
17	8 9 16	ciin	|- |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) )
18	6 17	cin	|- ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) )
19	3 7 18	cmpt	|- ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) )
20	1 2 19	cmpt	|- ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )
21	0 20	wceq	|- _|_P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )