Definition df-lsatoms 38957

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 38955	. 2 class LSAtoms
2		vw	. . 3 setvar 𝑤
3		cvv 3477	. . 3 class V
4		vv	. . . . 5 setvar 𝑣
5	2	cv 1535	. . . . . . 7 class 𝑤
6		cbs 17244	. . . . . . 7 class Base
7	5, 6	cfv 6562	. . . . . 6 class (Base‘𝑤)
8		c0g 17485	. . . . . . . 8 class 0g
9	5, 8	cfv 6562	. . . . . . 7 class (0g‘𝑤)
10	9	csn 4630	. . . . . 6 class {(0g‘𝑤)}
11	7, 10	cdif 3959	. . . . 5 class ((Base‘𝑤) ∖ {(0g‘𝑤)})
12	4	cv 1535	. . . . . . 7 class 𝑣
13	12	csn 4630	. . . . . 6 class {𝑣}
14		clspn 20986	. . . . . . 7 class LSpan
15	5, 14	cfv 6562	. . . . . 6 class (LSpan‘𝑤)
16	13, 15	cfv 6562	. . . . 5 class ((LSpan‘𝑤)‘{𝑣})
17	4, 11, 16	cmpt 5230	. . . 4 class (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))
18	17	crn 5689	. . 3 class ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣}))
19	2, 3, 18	cmpt 5230	. 2 class (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))
20	1, 19	wceq 1536	1 wff LSAtoms = (𝑤 ∈ V ↦ ran (𝑣 ∈ ((Base‘𝑤) ∖ {(0g‘𝑤)}) ↦ ((LSpan‘𝑤)‘{𝑣})))

This definition is referenced by:  lsatset  38971