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=BaseW
lsatset.n ⊢N=LSpan⁡W
lsatset.z ⊢0˙=0W
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=BaseW
2 lsatset.n ⊢N=LSpan⁡W
3 lsatset.z ⊢0˙=0W
4 lsatset.a ⊢A=LSAtoms⁡W
5 elex ⊢W∈X→W∈V
6 fveq2 ⊢w=W→Basew=BaseW
7 6 1 eqtr4di ⊢w=W→Basew=V
8 fveq2 ⊢w=W→0w=0W
9 8 3 eqtr4di ⊢w=W→0w=0˙
10 9 sneqd ⊢w=W→0w=0˙
11 7 10 difeq12d ⊢w=W→Basew∖0w=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∈Basew∖0w⟼LSpan⁡w⁡v=v∈V∖0˙⟼N⁡v
16 15 rneqd ⊢w=W→ran⁡v∈Basew∖0w⟼LSpan⁡w⁡v=ran⁡v∈V∖0˙⟼N⁡v
17 df-lsatoms ⊢LSAtoms=w∈V⟼ran⁡v∈Basew∖0w⟼LSpan⁡w⁡v
18 2 fvexi ⊢N∈V
19 18 rnex ⊢ran⁡N∈V
20 p0ex ⊢∅∈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