Theorem lssneln0

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

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

Proof

Step	Hyp	Ref	Expression
1		lssneln0.o	$$⊢\underset{\dot{}}{0}=0_W$$
2		lssneln0.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lssneln0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lssneln0.u	$$⊢\phi \to U\in S$$
5		lssneln0.x	$$⊢\phi \to X\in V$$
6		lssneln0.n	$$⊢\phi \to \neg X\in U$$
7	1 2 3 4 6	lssvneln0	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
8		eldifsn	$$⊢X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in V\wedge X\ne \underset{\dot{}}{0}\right)$$
9	5 7 8	sylanbrc	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$