Metamath Proof Explorer

Theorem lsatset

Description: The set of all 1-dim subspaces (atoms) of a left module or left vector space. (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses lsatset.v ⊢ V = Base W
lsatset.n ⊢ N = LSpan ⁡ W
lsatset.z ⊢ 0 ˙ = 0 W
lsatset.a ⊢ A = LSAtoms ⁡ W
Assertion lsatset ⊢ W ∈ X → A = ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v

Proof

Step Hyp Ref Expression
1 lsatset.v ⊢ V = Base W
2 lsatset.n ⊢ N = LSpan ⁡ W
3 lsatset.z ⊢ 0 ˙ = 0 W
4 lsatset.a ⊢ A = LSAtoms ⁡ W
5 elex ⊢ W ∈ X → W ∈ V
6 fveq2 ⊢ w = W → Base w = Base W
7 6 1 eqtr4di ⊢ w = W → Base w = V
8 fveq2 ⊢ w = W → 0 w = 0 W
9 8 3 eqtr4di ⊢ w = W → 0 w = 0 ˙
10 9 sneqd ⊢ w = W → 0 w = 0 ˙
11 7 10 difeq12d ⊢ w = W → Base w ∖ 0 w = V ∖ 0 ˙
12 fveq2 ⊢ w = W → LSpan ⁡ w = LSpan ⁡ W
13 12 2 eqtr4di ⊢ w = W → LSpan ⁡ w = N
14 13 fveq1d ⊢ w = W → LSpan ⁡ w ⁡ v = N ⁡ v
15 11 14 mpteq12dv ⊢ w = W → v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v = v ∈ V ∖ 0 ˙ ⟼ N ⁡ v
16 15 rneqd ⊢ w = W → ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v = ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v
17 df-lsatoms ⊢ LSAtoms = w ∈ V ⟼ ran ⁡ v ∈ Base w ∖ 0 w ⟼ LSpan ⁡ w ⁡ v
18 2 fvexi ⊢ N ∈ V
19 18 rnex ⊢ ran ⁡ N ∈ V
20 snex ⊢ ∅ ∈ V
21 19 20 unex ⊢ ran ⁡ N ∪ ∅ ∈ V
22 eqid ⊢ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v = v ∈ V ∖ 0 ˙ ⟼ N ⁡ v
23 fvrn0 ⊢ N ⁡ v ∈ ran ⁡ N ∪ ∅
24 23 a1i ⊢ v ∈ V ∖ 0 ˙ → N ⁡ v ∈ ran ⁡ N ∪ ∅
25 22 24 fmpti ⊢ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v : V ∖ 0 ˙ ⟶ ran ⁡ N ∪ ∅
26 frn ⊢ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v : V ∖ 0 ˙ ⟶ ran ⁡ N ∪ ∅ → ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v ⊆ ran ⁡ N ∪ ∅
27 25 26 ax-mp ⊢ ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v ⊆ ran ⁡ N ∪ ∅
28 21 27 ssexi ⊢ ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v ∈ V
29 16 17 28 fvmpt ⊢ W ∈ V → LSAtoms ⁡ W = ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v
30 5 29 syl ⊢ W ∈ X → LSAtoms ⁡ W = ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v
31 4 30 eqtrid ⊢ W ∈ X → A = ran ⁡ v ∈ V ∖ 0 ˙ ⟼ N ⁡ v