# Metamath Proof Explorer

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