# Metamath Proof Explorer

## Theorem lshpnel

Description: A hyperplane's generating vector does not belong to the hyperplane. (Contributed by NM, 3-Jul-2014)

Ref Expression
Hypotheses lshpnel.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lshpnel.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
lshpnel.p
lshpnel.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
lshpnel.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
lshpnel.u ${⊢}{\phi }\to {U}\in {H}$
lshpnel.x ${⊢}{\phi }\to {X}\in {V}$
lshpnel.e
Assertion lshpnel ${⊢}{\phi }\to ¬{X}\in {U}$

### Proof

Step Hyp Ref Expression
1 lshpnel.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lshpnel.n ${⊢}{N}=\mathrm{LSpan}\left({W}\right)$
3 lshpnel.p
4 lshpnel.h ${⊢}{H}=\mathrm{LSHyp}\left({W}\right)$
5 lshpnel.w ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
6 lshpnel.u ${⊢}{\phi }\to {U}\in {H}$
7 lshpnel.x ${⊢}{\phi }\to {X}\in {V}$
8 lshpnel.e
9 1 4 5 6 lshpne ${⊢}{\phi }\to {U}\ne {V}$
10 5 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {W}\in \mathrm{LMod}$
11 eqid ${⊢}\mathrm{LSubSp}\left({W}\right)=\mathrm{LSubSp}\left({W}\right)$
12 11 lsssssubg ${⊢}{W}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
13 10 12 syl ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to \mathrm{LSubSp}\left({W}\right)\subseteq \mathrm{SubGrp}\left({W}\right)$
14 11 4 5 6 lshplss ${⊢}{\phi }\to {U}\in \mathrm{LSubSp}\left({W}\right)$
15 14 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {U}\in \mathrm{LSubSp}\left({W}\right)$
16 13 15 sseldd ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {U}\in \mathrm{SubGrp}\left({W}\right)$
17 7 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {X}\in {V}$
18 1 11 2 lspsncl ${⊢}\left({W}\in \mathrm{LMod}\wedge {X}\in {V}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
19 10 17 18 syl2anc ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{LSubSp}\left({W}\right)$
20 13 19 sseldd ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {N}\left(\left\{{X}\right\}\right)\in \mathrm{SubGrp}\left({W}\right)$
21 simpr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {X}\in {U}$
22 11 2 10 15 21 lspsnel5a ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {N}\left(\left\{{X}\right\}\right)\subseteq {U}$
23 3 lsmss2
24 16 20 22 23 syl3anc
26 24 25 eqtr3d ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {U}={V}$
27 26 ex ${⊢}{\phi }\to \left({X}\in {U}\to {U}={V}\right)$
28 27 necon3ad ${⊢}{\phi }\to \left({U}\ne {V}\to ¬{X}\in {U}\right)$
29 9 28 mpd ${⊢}{\phi }\to ¬{X}\in {U}$