Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-polarityN Unicode version

Definition df-polarityN 29222
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  Atoms `  l ensures it is defined when  m  =  (/). (Contributed by NM, 23-Oct-2011.)
Assertion
Ref Expression
df-polarityN  |-  _|_ P  =  ( l  e. 
_V  |->  ( m  e. 
~P ( Atoms `  l
)  |->  ( ( Atoms `  l )  i^i  |^|_ p  e.  m  ( (
pmap `  l ) `  ( ( oc `  l ) `  p
) ) ) ) )
Distinct variable group:    m, l, p

Detailed syntax breakdown of Definition df-polarityN
StepHypRef Expression
1 cpolN 29221 . 2  class  _|_ P
2 vl . . 3  set  l
3 cvv 2740 . . 3  class  _V
4 vm . . . 4  set  m
52cv 1618 . . . . . 6  class  l
6 catm 28583 . . . . . 6  class  Atoms
75, 6cfv 4638 . . . . 5  class  ( Atoms `  l )
87cpw 3566 . . . 4  class  ~P ( Atoms `  l )
9 vp . . . . . 6  set  p
104cv 1618 . . . . . 6  class  m
119cv 1618 . . . . . . . 8  class  p
12 coc 13143 . . . . . . . . 9  class  oc
135, 12cfv 4638 . . . . . . . 8  class  ( oc
`  l )
1411, 13cfv 4638 . . . . . . 7  class  ( ( oc `  l ) `
 p )
15 cpmap 28816 . . . . . . . 8  class  pmap
165, 15cfv 4638 . . . . . . 7  class  ( pmap `  l )
1714, 16cfv 4638 . . . . . 6  class  ( (
pmap `  l ) `  ( ( oc `  l ) `  p
) )
189, 10, 17ciin 3847 . . . . 5  class  |^|_ p  e.  m  ( ( pmap `  l ) `  ( ( oc `  l ) `  p
) )
197, 18cin 3093 . . . 4  class  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) )
204, 8, 19cmpt 4017 . . 3  class  ( m  e.  ~P ( Atoms `  l )  |->  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) ) )
212, 3, 20cmpt 4017 . 2  class  ( l  e.  _V  |->  ( m  e.  ~P ( Atoms `  l )  |->  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) ) ) )
221, 21wceq 1619 1  wff  _|_ P  =  ( l  e. 
_V  |->  ( m  e. 
~P ( Atoms `  l
)  |->  ( ( Atoms `  l )  i^i  |^|_ p  e.  m  ( (
pmap `  l ) `  ( ( oc `  l ) `  p
) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  polfvalN  29223
  Copyright terms: Public domain W3C validator