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	$$⊢\mathrm{LSAtoms}=\left(w\in \mathrm{V}⟼\mathrm{ran}\left(v\in \left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)⟼\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsa	$$class\mathrm{LSAtoms}$$
1		vw	$$setvarw$$
2		cvv	$$class\mathrm{V}$$
3		vv	$$setvarv$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarw$$
6	5 4	cfv	$$class{\mathrm{Base}}_w$$
7		c0g	$$class{0}_{𝑔}$$
8	5 7	cfv	$$class{0}_w$$
9	8	csn	$$class\left\{0_w\right\}$$
10	6 9	cdif	$$class\left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)$$
11		clspn	$$class\mathrm{LSpan}$$
12	5 11	cfv	$$class\mathrm{LSpan}\left(w\right)$$
13	3	cv	$$setvarv$$
14	13	csn	$$class\left\{v\right\}$$
15	14 12	cfv	$$class\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)$$
16	3 10 15	cmpt	$$class\left(v\in \left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)⟼\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)\right)$$
17	16	crn	$$class\mathrm{ran}\left(v\in \left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)⟼\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)\right)$$
18	1 2 17	cmpt	$$class\left(w\in \mathrm{V}⟼\mathrm{ran}\left(v\in \left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)⟼\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)\right)\right)$$
19	0 18	wceq	$$wff\mathrm{LSAtoms}=\left(w\in \mathrm{V}⟼\mathrm{ran}\left(v\in \left({\mathrm{Base}}_w\setminus \left\{0_w\right\}\right)⟼\mathrm{LSpan}\left(w\right)\left(\left\{v\right\}\right)\right)\right)$$