Definition df-lsatoms 40299

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 = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))

Distinct variable group:   𝑤,𝑣

Detailed syntax breakdown of Definition df-lsatoms

Step	Hyp	Ref	Expression
1		clsa 40297	. 2 class LSAtoms
2		vw	. . 3 setvar 𝑤
3		cvv 3454	. . 3 class V
4		vv	. . . . 5 setvar 𝑣
5	2	cv 1569	. . . . . . 7 class 𝑤
6		cbs 17431	. . . . . . 7 class Base
7	5, 6	cfv 6566	. . . . . 6 class (Base‘𝑤)
8		c0g 17660	. . . . . . . 8 class 0g
9	5, 8	cfv 6566	. . . . . . 7 class (0g‘𝑤)
10	9	csn 4588	. . . . . 6 class {(0g‘𝑤)}
11	7, 10	cdif 4048	. . . . 5 class ((Base‘𝑤) ∖ {(0g‘𝑤)})
12	4	cv 1569	. . . . . . 7 class 𝑣
13	12	csn 4588	. . . . . 6 class {𝑣}
14		clspn 21297	. . . . . . 7 class LSpan
15	5, 14	cfv 6566	. . . . . 6 class (LSpan‘𝑤)
16	13, 15	cfv 6566	. . . . 5 class ((LSpan‘𝑤)‘{𝑣})
17	4, 11, 16	cmpt 5192	. . . 4 class (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))
18	17	crn 5659	. . 3 class ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))
19	2, 3, 18	cmpt 5192	. 2 class (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))
20	1, 19	wceq 1570	1 wff LSAtoms = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))

This definition is used by:  lsatset  40313