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={\mathrm{Base}}_W$$
	lsator0sp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lsator0sp.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsator0sp.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
	isator0sp.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	isator0sp.x	$$⊢\phi \to X\in V$$
Assertion	lsator0sp	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\in A\vee N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lsator0sp.v	$$⊢V={\mathrm{Base}}_W$$
2		lsator0sp.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lsator0sp.o	$$⊢\underset{\dot{}}{0}=0_W$$
4		lsator0sp.a	$$⊢A=\mathrm{LSAtoms}\left(W\right)$$
5		isator0sp.w	$$⊢\phi \to W\in \mathrm{LMod}$$
6		isator0sp.x	$$⊢\phi \to X\in V$$
7	1 2 3 4 5 6	lsatspn0	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\in A\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
8	7	biimprd	$$⊢\phi \to \left(X\ne \underset{\dot{}}{0}\to N\left(\left\{X\right\}\right)\in A\right)$$
9	8	necon1bd	$$⊢\phi \to \left(\neg N\left(\left\{X\right\}\right)\in A\to X=\underset{\dot{}}{0}\right)$$
10	1 3 2	lspsneq0	$$⊢\left(W\in \mathrm{LMod}\wedge X\in V\right)\to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
11	5 6 10	syl2anc	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
12	9 11	sylibrd	$$⊢\phi \to \left(\neg N\left(\left\{X\right\}\right)\in A\to N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$
13	12	orrd	$$⊢\phi \to \left(N\left(\left\{X\right\}\right)\in A\vee N\left(\left\{X\right\}\right)=\left\{\underset{\dot{}}{0}\right\}\right)$$