This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-lsatoms

Description: Define the set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014)

Ref Expression
Assertion df-lsatoms 
|- LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsa 
 |-  LSAtoms
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vv 
 |-  v
4 cbs 
 |-  Base
5 1 cv 
 |-  w
6 5 4 cfv 
 |-  ( Base ` w )
7 c0g 
 |-  0g
8 5 7 cfv 
 |-  ( 0g ` w )
9 8 csn 
 |-  { ( 0g ` w ) }
10 6 9 cdif 
 |-  ( ( Base ` w ) \ { ( 0g ` w ) } )
11 clspn 
 |-  LSpan
12 5 11 cfv 
 |-  ( LSpan ` w )
13 3 cv 
 |-  v
14 13 csn 
 |-  { v }
15 14 12 cfv 
 |-  ( ( LSpan ` w ) ` { v } )
16 3 10 15 cmpt 
 |-  ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) )
17 16 crn 
 |-  ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) )
18 1 2 17 cmpt 
 |-  ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )
19 0 18 wceq 
 |-  LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )