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

Definition df-lpolN 30938
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 30937 . 2  class LPol
2 vw . . 3  set  w
3 cvv 2789 . . 3  class  _V
42cv 1623 . . . . . . . 8  class  w
5 cbs 13142 . . . . . . . 8  class  Base
64, 5cfv 5221 . . . . . . 7  class  ( Base `  w )
7 vo . . . . . . . 8  set  o
87cv 1623 . . . . . . 7  class  o
96, 8cfv 5221 . . . . . 6  class  ( o `
 ( Base `  w
) )
10 c0g 13394 . . . . . . . 8  class  0g
114, 10cfv 5221 . . . . . . 7  class  ( 0g
`  w )
1211csn 3641 . . . . . 6  class  { ( 0g `  w ) }
139, 12wceq 1624 . . . . 5  wff  ( o `
 ( Base `  w
) )  =  {
( 0g `  w
) }
14 vx . . . . . . . . . . 11  set  x
1514cv 1623 . . . . . . . . . 10  class  x
1615, 6wss 3153 . . . . . . . . 9  wff  x  C_  ( Base `  w )
17 vy . . . . . . . . . . 11  set  y
1817cv 1623 . . . . . . . . . 10  class  y
1918, 6wss 3153 . . . . . . . . 9  wff  y  C_  ( Base `  w )
2015, 18wss 3153 . . . . . . . . 9  wff  x  C_  y
2116, 19, 20w3a 936 . . . . . . . 8  wff  ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )
2218, 8cfv 5221 . . . . . . . . 9  class  ( o `
 y )
2315, 8cfv 5221 . . . . . . . . 9  class  ( o `
 x )
2422, 23wss 3153 . . . . . . . 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 1528 . . . . . 6  wff  A. y
( ( x  C_  ( Base `  w )  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  (
o `  y )  C_  ( o `  x
) )
2726, 14wal 1528 . . . . 5  wff  A. x A. y ( ( x 
C_  ( Base `  w
)  /\  y  C_  ( Base `  w )  /\  x  C_  y )  ->  ( o `  y )  C_  (
o `  x )
)
28 clsh 28432 . . . . . . . . 9  class LSHyp
294, 28cfv 5221 . . . . . . . 8  class  (LSHyp `  w )
3023, 29wcel 1685 . . . . . . 7  wff  ( o `
 x )  e.  (LSHyp `  w )
3123, 8cfv 5221 . . . . . . . 8  class  ( o `
 ( o `  x ) )
3231, 15wceq 1624 . . . . . . 7  wff  ( o `
 ( o `  x ) )  =  x
3330, 32wa 360 . . . . . 6  wff  ( ( o `  x )  e.  (LSHyp `  w
)  /\  ( o `  ( o `  x
) )  =  x )
34 clsa 28431 . . . . . . 7  class LSAtoms
354, 34cfv 5221 . . . . . 6  class  (LSAtoms `  w
)
3633, 14, 35wral 2544 . . . . 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 15683 . . . . . 6  class  LSubSp
394, 38cfv 5221 . . . . 5  class  ( LSubSp `  w )
406cpw 3626 . . . . 5  class  ~P ( Base `  w )
41 cmap 6767 . . . . 5  class  ^m
4239, 40, 41co 5819 . . . 4  class  ( (
LSubSp `  w )  ^m  ~P ( Base `  w
) )
4337, 7, 42crab 2548 . . 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 4078 . 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 1624 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  30939
  Copyright terms: Public domain W3C validator