This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑤 ) ‘ { 𝑣 } ) ) )