Definition df-lsatoms 34263

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

Step	Hyp	Ref	Expression
1		clsa 34261	. 2 class LSAtoms
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vv	. . . . 5 setvar v
5	2	cv 1482	. . . . . . 7 class w
6		cbs 15857	. . . . . . 7 class Base
7	5, 6	cfv 5888	. . . . . 6 class ( Base ` w )
8		c0g 16100	. . . . . . . 8 class 0g
9	5, 8	cfv 5888	. . . . . . 7 class ( 0g ` w )
10	9	csn 4177	. . . . . 6 class { ( 0g ` w ) }
11	7, 10	cdif 3571	. . . . 5 class ( ( Base ` w ) \ { ( 0g ` w ) } )
12	4	cv 1482	. . . . . . 7 class v
13	12	csn 4177	. . . . . 6 class { v }
14		clspn 18971	. . . . . . 7 class LSpan
15	5, 14	cfv 5888	. . . . . 6 class ( LSpan ` w )
16	13, 15	cfv 5888	. . . . 5 class ( ( LSpan ` w ) ` { v } )
17	4, 11, 16	cmpt 4729	. . . 4 class ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) )
18	17	crn 5115	. . 3 class ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) )
19	2, 3, 18	cmpt 4729	. 2 class ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )
20	1, 19	wceq 1483	1 wff LSAtoms = ( w e. _V |-> ran ( v e. ( ( Base ` w ) \ { ( 0g ` w ) } ) |-> ( ( LSpan ` w ) ` { v } ) ) )

This definition is referenced by:  lsatset  34277