Theorem lsatssv

Description: An atom is a set of vectors. (Contributed by NM, 27-Feb-2015)

	Ref	Expression
Hypotheses	lsatssv.v	|- V = ( Base ` W )
	lsatssv.a	|- A = ( LSAtoms ` W )
	lsatssv.w	|- ( ph -> W e. LMod )
	lsatssv.g	|- ( ph -> Q e. A )
Assertion	lsatssv	|- ( ph -> Q C_ V )

Proof

Step	Hyp	Ref	Expression
1		lsatssv.v	|- V = ( Base ` W )
2		lsatssv.a	|- A = ( LSAtoms ` W )
3		lsatssv.w	|- ( ph -> W e. LMod )
4		lsatssv.g	|- ( ph -> Q e. A )
5		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
6	5 2 3 4	lsatlssel	|- ( ph -> Q e. ( LSubSp ` W ) )
7	1 5	lssss	|- ( Q e. ( LSubSp ` W ) -> Q C_ V )
8	6 7	syl	|- ( ph -> Q C_ V )