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=\mathrm{LSubSp}\left(W\right)$$
	lsatlss.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
Assertion	lsatlss	$$⊢W\in \mathrm{LMod}\to A\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		lsatlss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
2		lsatlss.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
5		eqid	$$⊢0_W=0_W$$
6	3 4 5 2	lsatset	$$⊢W\in \mathrm{LMod}\to A=\mathrm{ran}\left(v\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)⟼\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right)$$
7		eldifi	$$⊢v\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)\to v\in {\mathrm{Base}}_W$$
8	3 1 4	lspsncl	$$⊢\left(W\in \mathrm{LMod}\wedge v\in {\mathrm{Base}}_W\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\in S$$
9	7 8	sylan2	$$⊢\left(W\in \mathrm{LMod}\wedge v\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)\right)\to \mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\in S$$
10	9	fmpttd	$$⊢W\in \mathrm{LMod}\to \left(v\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)⟼\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right):{\mathrm{Base}}_W\setminus \left\{0_W\right\}⟶S$$
11	10	frnd	$$⊢W\in \mathrm{LMod}\to \mathrm{ran}\left(v\in \left({\mathrm{Base}}_W\setminus \left\{0_W\right\}\right)⟼\mathrm{LSpan}\left(W\right)\left(\left\{v\right\}\right)\right)\subseteq S$$
12	6 11	eqsstrd	$$⊢W\in \mathrm{LMod}\to A\subseteq S$$