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

Definition df-lpolN 31740
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
StepHypRef Expression
1 clpoN 31739 . 2  class LPol
2 vw . . 3  set  w
3 cvv 2864 . . 3  class  _V
42cv 1641 . . . . . . . 8  class  w
5 cbs 13245 . . . . . . . 8  class  Base
64, 5cfv 5337 . . . . . . 7  class  ( Base `  w )
7 vo . . . . . . . 8  set  o
87cv 1641 . . . . . . 7  class  o
96, 8cfv 5337 . . . . . 6  class  ( o `
 ( Base `  w
) )
10 c0g 13499 . . . . . . . 8  class  0g
114, 10cfv 5337 . . . . . . 7  class  ( 0g
`  w )
1211csn 3716 . . . . . 6  class  { ( 0g `  w ) }
139, 12wceq 1642 . . . . 5  wff  ( o `
 ( Base `  w
) )  =  {
( 0g `  w
) }
14 vx . . . . . . . . . . 11  set  x
1514cv 1641 . . . . . . . . . 10  class  x
1615, 6wss 3228 . . . . . . . . 9  wff  x  C_  ( Base `  w )
17 vy . . . . . . . . . . 11  set  y
1817cv 1641 . . . . . . . . . 10  class  y
1918, 6wss 3228 . . . . . . . . 9  wff  y  C_  ( Base `  w )
2015, 18wss 3228 . . . . . . . . 9  wff  x  C_  y
2116, 19, 20w3a 934 . . . . . . . 8  wff  ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )
2218, 8cfv 5337 . . . . . . . . 9  class  ( o `
 y )
2315, 8cfv 5337 . . . . . . . . 9  class  ( o `
 x )
2422, 23wss 3228 . . . . . . . 8  wff  ( o `
 y )  C_  ( o `  x
)
2521, 24wi 4 . . . . . . 7  wff  ( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w
)  /\  x  C_  y
)  ->  ( o `  y )  C_  (
o `  x )
)
2625, 17wal 1540 . . . . . 6  wff  A. y
( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  (
o `  y )  C_  ( o `  x
) )
2726, 14wal 1540 . . . . 5  wff  A. x A. y ( ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  ( o `  y )  C_  (
o `  x )
)
28 clsh 29234 . . . . . . . . 9  class LSHyp
294, 28cfv 5337 . . . . . . . 8  class  (LSHyp `  w )
3023, 29wcel 1710 . . . . . . 7  wff  ( o `
 x )  e.  (LSHyp `  w )
3123, 8cfv 5337 . . . . . . . 8  class  ( o `
 ( o `  x ) )
3231, 15wceq 1642 . . . . . . 7  wff  ( o `
 ( o `  x ) )  =  x
3330, 32wa 358 . . . . . 6  wff  ( ( o `  x )  e.  (LSHyp `  w
)  /\  ( o `  ( o `  x
) )  =  x )
34 clsa 29233 . . . . . . 7  class LSAtoms
354, 34cfv 5337 . . . . . 6  class  (LSAtoms `  w
)
3633, 14, 35wral 2619 . . . . 5  wff  A. x  e.  (LSAtoms `  w )
( ( o `  x )  e.  (LSHyp `  w )  /\  (
o `  ( o `  x ) )  =  x )
3713, 27, 36w3a 934 . . . 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 15788 . . . . . 6  class  LSubSp
394, 38cfv 5337 . . . . 5  class  ( LSubSp `  w )
406cpw 3701 . . . . 5  class  ~P ( Base `  w )
41 cmap 6860 . . . . 5  class  ^m
4239, 40, 41co 5945 . . . 4  class  ( (
LSubSp `  w )  ^m  ~P ( Base `  w
) )
4337, 7, 42crab 2623 . . 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 ) ) }
442, 3, 43cmpt 4158 . 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 ) ) } )
451, 44wceq 1642 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 ) ) } )
Colors of variables: wff set class
This definition is referenced by:  lpolsetN  31741
  Copyright terms: Public domain W3C validator