# Metamath Proof Explorer

## Theorem islshp

Description: The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014)

Ref Expression
Hypotheses lshpset.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lshpset.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lshpset.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lshpset.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
Assertion islshp ${⊢}{W}\in {X}\to \left({U}\in {H}↔\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$

### Proof

Step Hyp Ref Expression
1 lshpset.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lshpset.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lshpset.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
4 lshpset.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
5 1 2 3 4 lshpset ${⊢}{W}\in {X}\to {H}=\left\{{s}\in {S}|\left({s}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}\right)\right\}$
6 5 eleq2d ${⊢}{W}\in {X}\to \left({U}\in {H}↔{U}\in \left\{{s}\in {S}|\left({s}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}\right)\right\}\right)$
7 neeq1 ${⊢}{s}={U}\to \left({s}\ne {V}↔{U}\ne {V}\right)$
8 uneq1 ${⊢}{s}={U}\to {s}\cup \left\{{v}\right\}={U}\cup \left\{{v}\right\}$
9 8 fveqeq2d ${⊢}{s}={U}\to \left({N}\left({s}\cup \left\{{v}\right\}\right)={V}↔{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)$
10 9 rexbidv ${⊢}{s}={U}\to \left(\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}↔\exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)$
11 7 10 anbi12d ${⊢}{s}={U}\to \left(\left({s}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}\right)↔\left({U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$
12 11 elrab ${⊢}{U}\in \left\{{s}\in {S}|\left({s}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}\right)\right\}↔\left({U}\in {S}\wedge \left({U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$
13 3anass ${⊢}\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)↔\left({U}\in {S}\wedge \left({U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$
14 12 13 bitr4i ${⊢}{U}\in \left\{{s}\in {S}|\left({s}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({s}\cup \left\{{v}\right\}\right)={V}\right)\right\}↔\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)$
15 6 14 syl6bb ${⊢}{W}\in {X}\to \left({U}\in {H}↔\left({U}\in {S}\wedge {U}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{N}\left({U}\cup \left\{{v}\right\}\right)={V}\right)\right)$