Theorem lsatlssel

Description: An atom is a subspace. (Contributed by NM, 25-Aug-2014)

	Ref	Expression
Hypotheses	lsatlss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lsatlss.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	lssatssel.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lssatssel.u	$$⊢\phi \to U\in A$$
Assertion	lsatlssel	$$⊢\phi \to U\in 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		lssatssel.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lssatssel.u	$$⊢\phi \to U\in A$$
5	1 2	lsatlss	$$⊢W\in \mathrm{LMod}\to A\subseteq S$$
6	3 5	syl	$$⊢\phi \to A\subseteq S$$
7	6 4	sseldd	$$⊢\phi \to U\in S$$