This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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