Theorem lsatssn0

Description: A subspace (or any class) including an atom is nonzero. (Contributed by NM, 3-Feb-2015)

	Ref	Expression
Hypotheses	lsatssn0.o	|- .0. = ( 0g ` W )
	lsatssn0.a	|- A = ( LSAtoms ` W )
	lsatssn0.w	|- ( ph -> W e. LMod )
	lsatssn0.q	|- ( ph -> Q e. A )
	lsatssn0.u	|- ( ph -> Q C_ U )
Assertion	lsatssn0	|- ( ph -> U =/= { .0. } )

Proof

Step	Hyp	Ref	Expression
1		lsatssn0.o	|- .0. = ( 0g ` W )
2		lsatssn0.a	|- A = ( LSAtoms ` W )
3		lsatssn0.w	|- ( ph -> W e. LMod )
4		lsatssn0.q	|- ( ph -> Q e. A )
5		lsatssn0.u	|- ( ph -> Q C_ U )
6		eqid	|- ( LSubSp ` W ) = ( LSubSp ` W )
7	6 2 3 4	lsatlssel	|- ( ph -> Q e. ( LSubSp ` W ) )
8	1 6	lss0ss	|- ( ( W e. LMod /\ Q e. ( LSubSp ` W ) ) -> { .0. } C_ Q )
9	3 7 8	syl2anc	|- ( ph -> { .0. } C_ Q )
10	1 2 3 4	lsatn0	|- ( ph -> Q =/= { .0. } )
11	10	necomd	|- ( ph -> { .0. } =/= Q )
12		df-pss	|- ( { .0. } C. Q <-> ( { .0. } C_ Q /\ { .0. } =/= Q ) )
13	9 11 12	sylanbrc	|- ( ph -> { .0. } C. Q )
14	13 5	psssstrd	|- ( ph -> { .0. } C. U )
15	14	pssned	|- ( ph -> { .0. } =/= U )
16	15	necomd	|- ( ph -> U =/= { .0. } )