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 } ) ) )