Metamath Proof Explorer


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. } )