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

Definition df-polarityN 33886
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 33885 . 2  class  _|_P
2 vl . . 3  setvar  l
3 cvv 3078 . . 3  class  _V
4 vm . . . 4  setvar  m
52cv 1369 . . . . . 6  class  l
6 catm 33247 . . . . . 6  class  Atoms
75, 6cfv 5527 . . . . 5  class  ( Atoms `  l )
87cpw 3969 . . . 4  class  ~P ( Atoms `  l )
9 vp . . . . . 6  setvar  p
104cv 1369 . . . . . 6  class  m
119cv 1369 . . . . . . . 8  class  p
12 coc 14366 . . . . . . . . 9  class  oc
135, 12cfv 5527 . . . . . . . 8  class  ( oc
`  l )
1411, 13cfv 5527 . . . . . . 7  class  ( ( oc `  l ) `
 p )
15 cpmap 33480 . . . . . . . 8  class  pmap
165, 15cfv 5527 . . . . . . 7  class  ( pmap `  l )
1714, 16cfv 5527 . . . . . 6  class  ( (
pmap `  l ) `  ( ( oc `  l ) `  p
) )
189, 10, 17ciin 4281 . . . . 5  class  |^|_ p  e.  m  ( ( pmap `  l ) `  ( ( oc `  l ) `  p
) )
197, 18cin 3436 . . . 4  class  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) )
204, 8, 19cmpt 4459 . . 3  class  ( m  e.  ~P ( Atoms `  l )  |->  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) ) )
212, 3, 20cmpt 4459 . 2  class  ( l  e.  _V  |->  ( m  e.  ~P ( Atoms `  l )  |->  ( (
Atoms `  l )  i^i  |^|_ p  e.  m  ( ( pmap `  l
) `  ( ( oc `  l ) `  p ) ) ) ) )
221, 21wceq 1370 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 setvar class
This definition is referenced by:  polfvalN  33887
  Copyright terms: Public domain W3C validator