Theorem lshpne

Description: A hyperplane is not equal to the vector space. (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	lshpne.v	$$⊢V={\mathrm{Base}}_W$$
	lshpne.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshpne.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lshpne.u	$$⊢\phi \to U\in H$$
Assertion	lshpne	$$⊢\phi \to U\ne V$$

Proof

Step	Hyp	Ref	Expression
1		lshpne.v	$$⊢V={\mathrm{Base}}_W$$
2		lshpne.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
3		lshpne.w	$$⊢\phi \to W\in \mathrm{LMod}$$
4		lshpne.u	$$⊢\phi \to U\in H$$
5		eqid	$$⊢\mathrm{LSpan}\left(W\right)=\mathrm{LSpan}\left(W\right)$$
6		eqid	$$⊢\mathrm{LSubSp}\left(W\right)=\mathrm{LSubSp}\left(W\right)$$
7	1 5 6 2	islshp	$$⊢W\in \mathrm{LMod}\to \left(U\in H\leftrightarrow \left(U\in \mathrm{LSubSp}\left(W\right)\wedge U\ne V\wedge \exists v\in V\mathrm{LSpan}\left(W\right)\left(U\cup \left\{v\right\}\right)=V\right)\right)$$
8	3 7	syl	$$⊢\phi \to \left(U\in H\leftrightarrow \left(U\in \mathrm{LSubSp}\left(W\right)\wedge U\ne V\wedge \exists v\in V\mathrm{LSpan}\left(W\right)\left(U\cup \left\{v\right\}\right)=V\right)\right)$$
9	4 8	mpbid	$$⊢\phi \to \left(U\in \mathrm{LSubSp}\left(W\right)\wedge U\ne V\wedge \exists v\in V\mathrm{LSpan}\left(W\right)\left(U\cup \left\{v\right\}\right)=V\right)$$
10	9	simp2d	$$⊢\phi \to U\ne V$$