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

Definition df-lsatoms 29166
Description: Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014.)
Assertion
Ref Expression
df-lsatoms  |- LSAtoms  =  ( w  e.  _V  |->  ran  ( v  e.  ( ( Base `  w
)  \  { ( 0g `  w ) } )  |->  ( ( LSpan `  w ) `  {
v } ) ) )
Distinct variable group:    w, v

Detailed syntax breakdown of Definition df-lsatoms
StepHypRef Expression
1 clsa 29164 . 2  class LSAtoms
2 vw . . 3  set  w
3 cvv 2788 . . 3  class  _V
4 vv . . . . 5  set  v
52cv 1622 . . . . . . 7  class  w
6 cbs 13148 . . . . . . 7  class  Base
75, 6cfv 5255 . . . . . 6  class  ( Base `  w )
8 c0g 13400 . . . . . . . 8  class  0g
95, 8cfv 5255 . . . . . . 7  class  ( 0g
`  w )
109csn 3640 . . . . . 6  class  { ( 0g `  w ) }
117, 10cdif 3149 . . . . 5  class  ( (
Base `  w )  \  { ( 0g `  w ) } )
124cv 1622 . . . . . . 7  class  v
1312csn 3640 . . . . . 6  class  { v }
14 clspn 15728 . . . . . . 7  class  LSpan
155, 14cfv 5255 . . . . . 6  class  ( LSpan `  w )
1613, 15cfv 5255 . . . . 5  class  ( (
LSpan `  w ) `  { v } )
174, 11, 16cmpt 4077 . . . 4  class  ( v  e.  ( ( Base `  w )  \  {
( 0g `  w
) } )  |->  ( ( LSpan `  w ) `  { v } ) )
1817crn 4690 . . 3  class  ran  (
v  e.  ( (
Base `  w )  \  { ( 0g `  w ) } ) 
|->  ( ( LSpan `  w
) `  { v } ) )
192, 3, 18cmpt 4077 . 2  class  ( w  e.  _V  |->  ran  (
v  e.  ( (
Base `  w )  \  { ( 0g `  w ) } ) 
|->  ( ( LSpan `  w
) `  { v } ) ) )
201, 19wceq 1623 1  wff LSAtoms  =  ( w  e.  _V  |->  ran  ( v  e.  ( ( Base `  w
)  \  { ( 0g `  w ) } )  |->  ( ( LSpan `  w ) `  {
v } ) ) )
Colors of variables: wff set class
This definition is referenced by:  lsatset  29180
  Copyright terms: Public domain W3C validator