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

Definition df-lshyp 32945
Description: Define the set of all hyperplanes of a left module or left vector space. Also called co-atoms, these are subspaces that are one dimension less that the full space. (Contributed by NM, 29-Jun-2014.)
Assertion
Ref Expression
df-lshyp  |- LSHyp  =  ( w  e.  _V  |->  { s  e.  ( LSubSp `  w )  |  ( s  =/=  ( Base `  w )  /\  E. v  e.  ( Base `  w ) ( (
LSpan `  w ) `  ( s  u.  {
v } ) )  =  ( Base `  w
) ) } )
Distinct variable group:    v, s, w

Detailed syntax breakdown of Definition df-lshyp
StepHypRef Expression
1 clsh 32943 . 2  class LSHyp
2 vw . . 3  setvar  w
3 cvv 3076 . . 3  class  _V
4 vs . . . . . . 7  setvar  s
54cv 1369 . . . . . 6  class  s
62cv 1369 . . . . . . 7  class  w
7 cbs 14291 . . . . . . 7  class  Base
86, 7cfv 5525 . . . . . 6  class  ( Base `  w )
95, 8wne 2647 . . . . 5  wff  s  =/=  ( Base `  w
)
10 vv . . . . . . . . . . 11  setvar  v
1110cv 1369 . . . . . . . . . 10  class  v
1211csn 3984 . . . . . . . . 9  class  { v }
135, 12cun 3433 . . . . . . . 8  class  ( s  u.  { v } )
14 clspn 17174 . . . . . . . . 9  class  LSpan
156, 14cfv 5525 . . . . . . . 8  class  ( LSpan `  w )
1613, 15cfv 5525 . . . . . . 7  class  ( (
LSpan `  w ) `  ( s  u.  {
v } ) )
1716, 8wceq 1370 . . . . . 6  wff  ( (
LSpan `  w ) `  ( s  u.  {
v } ) )  =  ( Base `  w
)
1817, 10, 8wrex 2799 . . . . 5  wff  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
)
199, 18wa 369 . . . 4  wff  ( s  =/=  ( Base `  w
)  /\  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
) )
20 clss 17135 . . . . 5  class  LSubSp
216, 20cfv 5525 . . . 4  class  ( LSubSp `  w )
2219, 4, 21crab 2802 . . 3  class  { s  e.  ( LSubSp `  w
)  |  ( s  =/=  ( Base `  w
)  /\  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
) ) }
232, 3, 22cmpt 4457 . 2  class  ( w  e.  _V  |->  { s  e.  ( LSubSp `  w
)  |  ( s  =/=  ( Base `  w
)  /\  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
) ) } )
241, 23wceq 1370 1  wff LSHyp  =  ( w  e.  _V  |->  { s  e.  ( LSubSp `  w )  |  ( s  =/=  ( Base `  w )  /\  E. v  e.  ( Base `  w ) ( (
LSpan `  w ) `  ( s  u.  {
v } ) )  =  ( Base `  w
) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  lshpset  32946
  Copyright terms: Public domain W3C validator