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

Definition df-lpolN 30838
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 30837 . 2  class LPol
2 vw . . 3  set  w
3 cvv 2763 . . 3  class  _V
42cv 1618 . . . . . . . 8  class  w
5 cbs 13110 . . . . . . . 8  class  Base
64, 5cfv 4673 . . . . . . 7  class  ( Base `  w )
7 vo . . . . . . . 8  set  o
87cv 1618 . . . . . . 7  class  o
96, 8cfv 4673 . . . . . 6  class  ( o `
 ( Base `  w
) )
10 c0g 13362 . . . . . . . 8  class  0g
114, 10cfv 4673 . . . . . . 7  class  ( 0g
`  w )
1211csn 3614 . . . . . 6  class  { ( 0g `  w ) }
139, 12wceq 1619 . . . . 5  wff  ( o `
 ( Base `  w
) )  =  {
( 0g `  w
) }
14 vx . . . . . . . . . . 11  set  x
1514cv 1618 . . . . . . . . . 10  class  x
1615, 6wss 3127 . . . . . . . . 9  wff  x  C_  ( Base `  w )
17 vy . . . . . . . . . . 11  set  y
1817cv 1618 . . . . . . . . . 10  class  y
1918, 6wss 3127 . . . . . . . . 9  wff  y  C_  ( Base `  w )
2015, 18wss 3127 . . . . . . . . 9  wff  x  C_  y
2116, 19, 20w3a 939 . . . . . . . 8  wff  ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )
2218, 8cfv 4673 . . . . . . . . 9  class  ( o `
 y )
2315, 8cfv 4673 . . . . . . . . 9  class  ( o `
 x )
2422, 23wss 3127 . . . . . . . 8  wff  ( o `
 y )  C_  ( o `  x
)
2521, 24wi 6 . . . . . . 7  wff  ( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w
)  /\  x  C_  y
)  ->  ( o `  y )  C_  (
o `  x )
)
2625, 17wal 1532 . . . . . 6  wff  A. y
( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  (
o `  y )  C_  ( o `  x
) )
2726, 14wal 1532 . . . . 5  wff  A. x A. y ( ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  ( o `  y )  C_  (
o `  x )
)
28 clsh 28332 . . . . . . . . 9  class LSHyp
294, 28cfv 4673 . . . . . . . 8  class  (LSHyp `  w )
3023, 29wcel 1621 . . . . . . 7  wff  ( o `
 x )  e.  (LSHyp `  w )
3123, 8cfv 4673 . . . . . . . 8  class  ( o `
 ( o `  x ) )
3231, 15wceq 1619 . . . . . . 7  wff  ( o `
 ( o `  x ) )  =  x
3330, 32wa 360 . . . . . 6  wff  ( ( o `  x )  e.  (LSHyp `  w
)  /\  ( o `  ( o `  x
) )  =  x )
34 clsa 28331 . . . . . . 7  class LSAtoms
354, 34cfv 4673 . . . . . 6  class  (LSAtoms `  w
)
3633, 14, 35wral 2518 . . . . 5  wff  A. x  e.  (LSAtoms `  w )
( ( o `  x )  e.  (LSHyp `  w )  /\  (
o `  ( o `  x ) )  =  x )
3713, 27, 36w3a 939 . . . 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 15651 . . . . . 6  class  LSubSp
394, 38cfv 4673 . . . . 5  class  ( LSubSp `  w )
406cpw 3599 . . . . 5  class  ~P ( Base `  w )
41 cmap 6740 . . . . 5  class  ^m
4239, 40, 41co 5792 . . . 4  class  ( (
LSubSp `  w )  ^m  ~P ( Base `  w
) )
4337, 7, 42crab 2522 . . 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 4051 . 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 1619 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  30839
  Copyright terms: Public domain W3C validator