Metamath Proof Explorer

Theorem lsatlss

Description: The set of 1-dim subspaces is a set of subspaces. (Contributed by NM, 9-Apr-2014) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses lsatlss.s ⊢ S = LSubSp ⁡ W
lsatlss.a ⊢ A = LSAtoms ⁡ W
Assertion lsatlss ⊢ W ∈ LMod → A ⊆ S

Proof

Step Hyp Ref Expression
1 lsatlss.s ⊢ S = LSubSp ⁡ W
2 lsatlss.a ⊢ A = LSAtoms ⁡ W
3 eqid ⊢ Base W = Base W
4 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
5 eqid ⊢ 0 W = 0 W
6 3 4 5 2 lsatset ⊢ W ∈ LMod → A = ran ⁡ v ∈ Base W ∖ 0 W ⟼ LSpan ⁡ W ⁡ v
7 eldifi ⊢ v ∈ Base W ∖ 0 W → v ∈ Base W
8 3 1 4 lspsncl ⊢ W ∈ LMod ∧ v ∈ Base W → LSpan ⁡ W ⁡ v ∈ S
9 7 8 sylan2 ⊢ W ∈ LMod ∧ v ∈ Base W ∖ 0 W → LSpan ⁡ W ⁡ v ∈ S
10 9 fmpttd ⊢ W ∈ LMod → v ∈ Base W ∖ 0 W ⟼ LSpan ⁡ W ⁡ v : Base W ∖ 0 W ⟶ S
11 10 frnd ⊢ W ∈ LMod → ran ⁡ v ∈ Base W ∖ 0 W ⟼ LSpan ⁡ W ⁡ v ⊆ S
12 6 11 eqsstrd ⊢ W ∈ LMod → A ⊆ S