# Metamath Proof Explorer

## 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}↔\left({U}\in {S}\wedge {U}\ne {\mathrm{Base}}_{{W}}\wedge \exists {v}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\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}↔\left({U}\in {S}\wedge {U}\ne {\mathrm{Base}}_{{W}}\wedge \exists {v}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\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}}\phantom{\rule{.4em}{0ex}}\mathrm{LSpan}\left({W}\right)\left({U}\cup \left\{{v}\right\}\right)={\mathrm{Base}}_{{W}}\right)$
10 9 simp1d ${⊢}{\phi }\to {U}\in {S}$