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

Definition df-lpolN 31671
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 31670 . 2  class LPol
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . . . . 8  class  w
5 cbs 13148 . . . . . . . 8  class  Base
64, 5cfv 5255 . . . . . . 7  class  ( Base `  w )
7 vo . . . . . . . 8  set  o
87cv 1622 . . . . . . 7  class  o
96, 8cfv 5255 . . . . . 6  class  ( o `
 ( Base `  w
) )
10 c0g 13400 . . . . . . . 8  class  0g
114, 10cfv 5255 . . . . . . 7  class  ( 0g
`  w )
1211csn 3640 . . . . . 6  class  { ( 0g `  w ) }
139, 12wceq 1623 . . . . 5  wff  ( o `
 ( Base `  w
) )  =  {
( 0g `  w
) }
14 vx . . . . . . . . . . 11  set  x
1514cv 1622 . . . . . . . . . 10  class  x
1615, 6wss 3152 . . . . . . . . 9  wff  x  C_  ( Base `  w )
17 vy . . . . . . . . . . 11  set  y
1817cv 1622 . . . . . . . . . 10  class  y
1918, 6wss 3152 . . . . . . . . 9  wff  y  C_  ( Base `  w )
2015, 18wss 3152 . . . . . . . . 9  wff  x  C_  y
2116, 19, 20w3a 934 . . . . . . . 8  wff  ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )
2218, 8cfv 5255 . . . . . . . . 9  class  ( o `
 y )
2315, 8cfv 5255 . . . . . . . . 9  class  ( o `
 x )
2422, 23wss 3152 . . . . . . . 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 1527 . . . . . 6  wff  A. y
( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  (
o `  y )  C_  ( o `  x
) )
2726, 14wal 1527 . . . . 5  wff  A. x A. y ( ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  ( o `  y )  C_  (
o `  x )
)
28 clsh 29165 . . . . . . . . 9  class LSHyp
294, 28cfv 5255 . . . . . . . 8  class  (LSHyp `  w )
3023, 29wcel 1684 . . . . . . 7  wff  ( o `
 x )  e.  (LSHyp `  w )
3123, 8cfv 5255 . . . . . . . 8  class  ( o `
 ( o `  x ) )
3231, 15wceq 1623 . . . . . . 7  wff  ( o `
 ( o `  x ) )  =  x
3330, 32wa 358 . . . . . 6  wff  ( ( o `  x )  e.  (LSHyp `  w
)  /\  ( o `  ( o `  x
) )  =  x )
34 clsa 29164 . . . . . . 7  class LSAtoms
354, 34cfv 5255 . . . . . 6  class  (LSAtoms `  w
)
3633, 14, 35wral 2543 . . . . 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 15689 . . . . . 6  class  LSubSp
394, 38cfv 5255 . . . . 5  class  ( LSubSp `  w )
406cpw 3625 . . . . 5  class  ~P ( Base `  w )
41 cmap 6772 . . . . 5  class  ^m
4239, 40, 41co 5858 . . . 4  class  ( (
LSubSp `  w )  ^m  ~P ( Base `  w
) )
4337, 7, 42crab 2547 . . 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 4077 . 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 1623 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  31672
  Copyright terms: Public domain W3C validator