Theorem lssvneln0

Description: A vector X which doesn't belong to a subspace U is nonzero. (Contributed by NM, 14-May-2015) (Revised by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lssvneln0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lssvneln0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lssvneln0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lssvneln0.u	$$⊢\phi \to U\in S$$
	lssvneln0.n	$$⊢\phi \to \neg X\in U$$
Assertion	lssvneln0	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lssvneln0.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lssvneln0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lssvneln0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lssvneln0.u	$$⊢\phi \to U\in S$$
5		lssvneln0.n	$$⊢\phi \to \neg X\in U$$
6	1 2	lss0cl	$$⊢\left(W\in \mathrm{LMod}\wedge U\in S\right)\to \underset{\dot{}}{0}\in U$$
7	3 4 6	syl2anc	$$⊢\phi \to \underset{\dot{}}{0}\in U$$
8		eleq1a	$$⊢\underset{\dot{}}{0}\in U\to \left(X=\underset{\dot{}}{0}\to X\in U\right)$$
9	7 8	syl	$$⊢\phi \to \left(X=\underset{\dot{}}{0}\to X\in U\right)$$
10	9	necon3bd	$$⊢\phi \to \left(\neg X\in U\to X\ne \underset{\dot{}}{0}\right)$$
11	5 10	mpd	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$