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 = w ∈ V ⟼ ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 clsa class LSAtoms
1 vw setvar w
2 cvv class V
3 vv setvar v
4 cbs class Base
5 1 cv setvar w
6 5 4 cfv class Base w
7 c0g class 0 𝑔
8 5 7 cfv class 0 w
9 8 csn class 0 w
10 6 9 cdif class Base w ∖ 0 w
11 clspn class LSpan
12 5 11 cfv class LSpan ⁡ w
13 3 cv setvar v
14 13 csn class v
15 14 12 cfv class LSpan ⁡ w ⁡ v
16 3 10 15 cmpt class v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v
17 16 crn class ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v
18 1 2 17 cmpt class w ∈ V ⟼ ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v
19 0 18 wceq wff LSAtoms = w ∈ V ⟼ ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v