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

Metamath Proof Explorer

Theorem lsator0sp

Description: The span of a vector is either an atom or the zero subspace. (Contributed by NM, 15-Mar-2015)

Ref Expression
Hypotheses lsator0sp.v 
|- V = ( Base ` W )
lsator0sp.n 
|- N = ( LSpan ` W )
lsator0sp.o 
|- .0. = ( 0g ` W )
lsator0sp.a 
|- A = ( LSAtoms ` W )
isator0sp.w 
|- ( ph -> W e. LMod )
isator0sp.x 
|- ( ph -> X e. V )
Assertion lsator0sp 
|- ( ph -> ( ( N ` { X } ) e. A \/ ( N ` { X } ) = { .0. } ) )

Proof

Step Hyp Ref Expression
1 lsator0sp.v 
 |-  V = ( Base ` W )
2 lsator0sp.n 
 |-  N = ( LSpan ` W )
3 lsator0sp.o 
 |-  .0. = ( 0g ` W )
4 lsator0sp.a 
 |-  A = ( LSAtoms ` W )
5 isator0sp.w 
 |-  ( ph -> W e. LMod )
6 isator0sp.x 
 |-  ( ph -> X e. V )
7 1 2 3 4 5 6 lsatspn0 
 |-  ( ph -> ( ( N ` { X } ) e. A <-> X =/= .0. ) )
8 7 biimprd 
 |-  ( ph -> ( X =/= .0. -> ( N ` { X } ) e. A ) )
9 8 necon1bd 
 |-  ( ph -> ( -. ( N ` { X } ) e. A -> X = .0. ) )
10 1 3 2 lspsneq0 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
11 5 6 10 syl2anc 
 |-  ( ph -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
12 9 11 sylibrd 
 |-  ( ph -> ( -. ( N ` { X } ) e. A -> ( N ` { X } ) = { .0. } ) )
13 12 orrd 
 |-  ( ph -> ( ( N ` { X } ) e. A \/ ( N ` { X } ) = { .0. } ) )