Theorem lsatlssel

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

	Ref	Expression
Hypotheses	lsatlss.s	|- S = ( LSubSp ` W )
	lsatlss.a	|- A = ( LSAtoms ` W )
	lssatssel.w	|- ( ph -> W e. LMod )
	lssatssel.u	|- ( ph -> U e. A )
Assertion	lsatlssel	|- ( ph -> U e. S )

Proof

Step	Hyp	Ref	Expression
1		lsatlss.s	|- S = ( LSubSp ` W )
2		lsatlss.a	|- A = ( LSAtoms ` W )
3		lssatssel.w	|- ( ph -> W e. LMod )
4		lssatssel.u	|- ( ph -> U e. A )
5	1 2	lsatlss	|- ( W e. LMod -> A C_ S )
6	3 5	syl	|- ( ph -> A C_ S )
7	6 4	sseldd	|- ( ph -> U e. S )