This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )