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

Definition df-lshyp 29167
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 29165 . 2  class LSHyp
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vs . . . . . . 7  set  s
54cv 1622 . . . . . 6  class  s
62cv 1622 . . . . . . 7  class  w
7 cbs 13148 . . . . . . 7  class  Base
86, 7cfv 5255 . . . . . 6  class  ( Base `  w )
95, 8wne 2446 . . . . 5  wff  s  =/=  ( Base `  w
)
10 vv . . . . . . . . . . 11  set  v
1110cv 1622 . . . . . . . . . 10  class  v
1211csn 3640 . . . . . . . . 9  class  { v }
135, 12cun 3150 . . . . . . . 8  class  ( s  u.  { v } )
14 clspn 15728 . . . . . . . . 9  class  LSpan
156, 14cfv 5255 . . . . . . . 8  class  ( LSpan `  w )
1613, 15cfv 5255 . . . . . . 7  class  ( (
LSpan `  w ) `  ( s  u.  {
v } ) )
1716, 8wceq 1623 . . . . . 6  wff  ( (
LSpan `  w ) `  ( s  u.  {
v } ) )  =  ( Base `  w
)
1817, 10, 8wrex 2544 . . . . 5  wff  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
)
199, 18wa 358 . . . 4  wff  ( s  =/=  ( Base `  w
)  /\  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
) )
20 clss 15689 . . . . 5  class  LSubSp
216, 20cfv 5255 . . . 4  class  ( LSubSp `  w )
2219, 4, 21crab 2547 . . 3  class  { s  e.  ( LSubSp `  w
)  |  ( s  =/=  ( Base `  w
)  /\  E. v  e.  ( Base `  w
) ( ( LSpan `  w ) `  (
s  u.  { v } ) )  =  ( Base `  w
) ) }
232, 3, 22cmpt 4077 . 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 1623 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 set class
This definition is referenced by:  lshpset  29168
  Copyright terms: Public domain W3C validator