Theorem lshplss

Description: A hyperplane is a subspace. (Contributed by NM, 3-Jul-2014)

	Ref	Expression
Hypotheses	lshplss.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lshplss.h	$$⊢H=\mathrm{LSHyp}\left(W\right)$$
	lshplss.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	lshplss.u	$$⊢\phi \to U\in H$$
Assertion	lshplss	$$⊢\phi \to U\in S$$

Proof

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