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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clsa	⊢ LSAtoms
1		vw	⊢ 𝑤
2		cvv	⊢ V
3		vv	⊢ 𝑣
4		cbs	⊢ Base
5	1	cv	⊢ 𝑤
6	5 4	cfv	⊢ ( Base ‘ 𝑤 )
7		c0g	⊢ 0g
8	5 7	cfv	⊢ ( 0g ‘ 𝑤 )
9	8	csn	⊢ { ( 0g ‘ 𝑤 ) }
10	6 9	cdif	⊢ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } )
11		clspn	⊢ LSpan
12	5 11	cfv	⊢ ( LSpan ‘ 𝑤 )
13	3	cv	⊢ 𝑣
14	13	csn	⊢ { 𝑣 }
15	14 12	cfv	⊢ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } )
16	3 10 15	cmpt	⊢ ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) )
17	16	crn	⊢ ran ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) )
18	1 2 17	cmpt	⊢ ( 𝑤 ∈ V ↦ ran ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) ) )
19	0 18	wceq	⊢ LSAtoms = ( 𝑤 ∈ V ↦ ran ( 𝑣 ∈ ( ( Base ‘ 𝑤 ) ∖ { ( 0g ‘ 𝑤 ) } ) ↦ ( ( LSpan ‘ 𝑤 ) ‘ { 𝑣 } ) ) )