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

Definition df-lpolN 31964
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 31963 . 2  class LPol
2 vw . . 3  set  w
3 cvv 2916 . . 3  class  _V
42cv 1648 . . . . . . . 8  class  w
5 cbs 13424 . . . . . . . 8  class  Base
64, 5cfv 5413 . . . . . . 7  class  ( Base `  w )
7 vo . . . . . . . 8  set  o
87cv 1648 . . . . . . 7  class  o
96, 8cfv 5413 . . . . . 6  class  ( o `
 ( Base `  w
) )
10 c0g 13678 . . . . . . . 8  class  0g
114, 10cfv 5413 . . . . . . 7  class  ( 0g
`  w )
1211csn 3774 . . . . . 6  class  { ( 0g `  w ) }
139, 12wceq 1649 . . . . 5  wff  ( o `
 ( Base `  w
) )  =  {
( 0g `  w
) }
14 vx . . . . . . . . . . 11  set  x
1514cv 1648 . . . . . . . . . 10  class  x
1615, 6wss 3280 . . . . . . . . 9  wff  x  C_  ( Base `  w )
17 vy . . . . . . . . . . 11  set  y
1817cv 1648 . . . . . . . . . 10  class  y
1918, 6wss 3280 . . . . . . . . 9  wff  y  C_  ( Base `  w )
2015, 18wss 3280 . . . . . . . . 9  wff  x  C_  y
2116, 19, 20w3a 936 . . . . . . . 8  wff  ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )
2218, 8cfv 5413 . . . . . . . . 9  class  ( o `
 y )
2315, 8cfv 5413 . . . . . . . . 9  class  ( o `
 x )
2422, 23wss 3280 . . . . . . . 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 1546 . . . . . 6  wff  A. y
( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  (
o `  y )  C_  ( o `  x
) )
2726, 14wal 1546 . . . . 5  wff  A. x A. y ( ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  ( o `  y )  C_  (
o `  x )
)
28 clsh 29458 . . . . . . . . 9  class LSHyp
294, 28cfv 5413 . . . . . . . 8  class  (LSHyp `  w )
3023, 29wcel 1721 . . . . . . 7  wff  ( o `
 x )  e.  (LSHyp `  w )
3123, 8cfv 5413 . . . . . . . 8  class  ( o `
 ( o `  x ) )
3231, 15wceq 1649 . . . . . . 7  wff  ( o `
 ( o `  x ) )  =  x
3330, 32wa 359 . . . . . 6  wff  ( ( o `  x )  e.  (LSHyp `  w
)  /\  ( o `  ( o `  x
) )  =  x )
34 clsa 29457 . . . . . . 7  class LSAtoms
354, 34cfv 5413 . . . . . 6  class  (LSAtoms `  w
)
3633, 14, 35wral 2666 . . . . 5  wff  A. x  e.  (LSAtoms `  w )
( ( o `  x )  e.  (LSHyp `  w )  /\  (
o `  ( o `  x ) )  =  x )
3713, 27, 36w3a 936 . . . 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 15963 . . . . . 6  class  LSubSp
394, 38cfv 5413 . . . . 5  class  ( LSubSp `  w )
406cpw 3759 . . . . 5  class  ~P ( Base `  w )
41 cmap 6977 . . . . 5  class  ^m
4239, 40, 41co 6040 . . . 4  class  ( (
LSubSp `  w )  ^m  ~P ( Base `  w
) )
4337, 7, 42crab 2670 . . 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 4226 . 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 1649 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  31965
  Copyright terms: Public domain W3C validator