Theorem lshpne0

Description: The member of the span in the hyperplane definition does not belong to the hyperplane. (Contributed by NM, 14-Jul-2014) (Proof shortened by AV, 19-Jul-2022)

	Ref	Expression
Hypotheses	lshpne0.v	$$⊢V={\mathrm{Base}}_W$$
	lshpne0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lshpne0.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
	lshpne0.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpne0.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lshpne0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lshpne0.u	$$⊢\phi \to U\in H$$
	lshpne0.x	$$⊢\phi \to X\in V$$
	lshpne0.e	$$⊢\phi \to U\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V$$
Assertion	lshpne0	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lshpne0.v	$$⊢V={\mathrm{Base}}_W$$
2		lshpne0.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
3		lshpne0.p	$$⊢\underset{\dot{}}{\oplus }=\mathrm{LSSum}\left(W\right)$$
4		lshpne0.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
5		lshpne0.o	$$⊢\underset{\dot{}}{0}=0_W$$
6		lshpne0.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		lshpne0.u	$$⊢\phi \to U\in H$$
8		lshpne0.x	$$⊢\phi \to X\in V$$
9		lshpne0.e	$$⊢\phi \to U\underset{\dot{}}{\oplus }N\left(\left\{X\right\}\right)=V$$
10		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
11	10 4 6 7	lshplss	$$⊢\phi \to U\in \mathrm{LSubSp}\left(W\right)$$
12	1 2 3 4 6 7 8 9	lshpnel	$$⊢\phi \to \neg X\in U$$
13	5 10 6 11 12	lssvneln0	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$