# Metamath Proof Explorer

## Theorem dochshpncl

Description: If a hyperplane is not closed, its closure equals the vector space. (Contributed by NM, 29-Oct-2014)

Ref Expression
Hypotheses dochshpncl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochshpncl.o
dochshpncl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochshpncl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochshpncl.y ${⊢}{Y}=\mathrm{LSHyp}\left({U}\right)$
dochshpncl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
dochshpncl.x ${⊢}{\phi }\to {X}\in {Y}$
Assertion dochshpncl

### Proof

Step Hyp Ref Expression
1 dochshpncl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochshpncl.o
3 dochshpncl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochshpncl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochshpncl.y ${⊢}{Y}=\mathrm{LSHyp}\left({U}\right)$
6 dochshpncl.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 dochshpncl.x ${⊢}{\phi }\to {X}\in {Y}$
8 eqid ${⊢}\mathrm{LSpan}\left({U}\right)=\mathrm{LSpan}\left({U}\right)$
9 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
10 eqid ${⊢}\mathrm{LSSum}\left({U}\right)=\mathrm{LSSum}\left({U}\right)$
11 1 3 6 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
12 4 8 9 10 5 11 islshpsm ${⊢}{\phi }\to \left({X}\in {Y}↔\left({X}\in \mathrm{LSubSp}\left({U}\right)\wedge {X}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{X}\mathrm{LSSum}\left({U}\right)\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)={V}\right)\right)$
13 7 12 mpbid ${⊢}{\phi }\to \left({X}\in \mathrm{LSubSp}\left({U}\right)\wedge {X}\ne {V}\wedge \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{X}\mathrm{LSSum}\left({U}\right)\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)={V}\right)$
14 13 simp3d ${⊢}{\phi }\to \exists {v}\in {V}\phantom{\rule{.4em}{0ex}}{X}\mathrm{LSSum}\left({U}\right)\mathrm{LSpan}\left({U}\right)\left(\left\{{v}\right\}\right)={V}$
16 id ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to \left({\phi }\wedge {v}\in {V}\right)$
19 9 5 11 7 lshplss ${⊢}{\phi }\to {X}\in \mathrm{LSubSp}\left({U}\right)$
20 4 9 lssss ${⊢}{X}\in \mathrm{LSubSp}\left({U}\right)\to {X}\subseteq {V}$
21 19 20 syl ${⊢}{\phi }\to {X}\subseteq {V}$
22 1 3 4 2 dochocss
23 6 21 22 syl2anc
26 simp1r
27 26 necomd
28 df-pss
29 25 27 28 sylanbrc
30 1 3 4 2 dochssv
31 6 21 30 syl2anc
32 1 3 4 2 dochssv
33 6 31 32 syl2anc
36 simp3
37 35 36 sseqtrrd
38 6 adantr ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
39 1 3 38 dvhlvec ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {U}\in \mathrm{LVec}$
40 19 adantr ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {X}\in \mathrm{LSubSp}\left({U}\right)$
41 1 3 4 9 2 dochlss
42 6 31 41 syl2anc
44 simpr ${⊢}\left({\phi }\wedge {v}\in {V}\right)\to {v}\in {V}$
51 4 5 11 7 lshpne ${⊢}{\phi }\to {X}\ne {V}$