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