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 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 syl5eq W X A = ran v V 0 ˙ N v