# 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 = ( LHyp ` K )`
dochshpncl.o
`|- ._|_ = ( ( ocH ` K ) ` W )`
dochshpncl.u
`|- U = ( ( DVecH ` K ) ` W )`
dochshpncl.v
`|- V = ( Base ` U )`
dochshpncl.y
`|- Y = ( LSHyp ` U )`
dochshpncl.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
dochshpncl.x
`|- ( ph -> X e. Y )`
Assertion dochshpncl
`|- ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) =/= X <-> ( ._|_ ` ( ._|_ ` X ) ) = V ) )`

### Proof

Step Hyp Ref Expression
1 dochshpncl.h
` |-  H = ( LHyp ` K )`
2 dochshpncl.o
` |-  ._|_ = ( ( ocH ` K ) ` W )`
3 dochshpncl.u
` |-  U = ( ( DVecH ` K ) ` W )`
4 dochshpncl.v
` |-  V = ( Base ` U )`
5 dochshpncl.y
` |-  Y = ( LSHyp ` U )`
6 dochshpncl.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
7 dochshpncl.x
` |-  ( ph -> X e. Y )`
8 eqid
` |-  ( LSpan ` U ) = ( LSpan ` U )`
9 eqid
` |-  ( LSubSp ` U ) = ( LSubSp ` U )`
10 eqid
` |-  ( LSSum ` U ) = ( LSSum ` U )`
11 1 3 6 dvhlmod
` |-  ( ph -> U e. LMod )`
12 4 8 9 10 5 11 islshpsm
` |-  ( ph -> ( X e. Y <-> ( X e. ( LSubSp ` U ) /\ X =/= V /\ E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) ) )`
13 7 12 mpbid
` |-  ( ph -> ( X e. ( LSubSp ` U ) /\ X =/= V /\ E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) )`
14 13 simp3d
` |-  ( ph -> E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V )`
16 id
` |-  ( ( ph /\ v e. V ) -> ( ph /\ v e. V ) )`
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V ) -> ( ph /\ v e. V ) )`
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ph /\ v e. V ) )`
19 9 5 11 7 lshplss
` |-  ( ph -> X e. ( LSubSp ` U ) )`
20 4 9 lssss
` |-  ( X e. ( LSubSp ` U ) -> X C_ V )`
21 19 20 syl
` |-  ( ph -> X C_ V )`
22 1 3 4 2 dochocss
` |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )`
23 6 21 22 syl2anc
` |-  ( ph -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )`
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )`
26 simp1r
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) =/= X )`
27 26 necomd
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> X =/= ( ._|_ ` ( ._|_ ` X ) ) )`
28 df-pss
` |-  ( X C. ( ._|_ ` ( ._|_ ` X ) ) <-> ( X C_ ( ._|_ ` ( ._|_ ` X ) ) /\ X =/= ( ._|_ ` ( ._|_ ` X ) ) ) )`
29 25 27 28 sylanbrc
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> X C. ( ._|_ ` ( ._|_ ` X ) ) )`
30 1 3 4 2 dochssv
` |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) C_ V )`
31 6 21 30 syl2anc
` |-  ( ph -> ( ._|_ ` X ) C_ V )`
32 1 3 4 2 dochssv
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ V )`
33 6 31 32 syl2anc
` |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) C_ V )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ V )`
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ V )`
36 simp3
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V )`
37 35 36 sseqtrrd
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) )`
` |-  ( ( ph /\ v e. V ) -> ( K e. HL /\ W e. H ) )`
39 1 3 38 dvhlvec
` |-  ( ( ph /\ v e. V ) -> U e. LVec )`
` |-  ( ( ph /\ v e. V ) -> X e. ( LSubSp ` U ) )`
41 1 3 4 9 2 dochlss
` |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ( LSubSp ` U ) )`
42 6 31 41 syl2anc
` |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) e. ( LSubSp ` U ) )`
` |-  ( ( ph /\ v e. V ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ( LSubSp ` U ) )`
44 simpr
` |-  ( ( ph /\ v e. V ) -> v e. V )`
45 4 9 8 10 39 40 43 44 lsmcv
` |-  ( ( ( ph /\ v e. V ) /\ X C. ( ._|_ ` ( ._|_ ` X ) ) /\ ( ._|_ ` ( ._|_ ` X ) ) C_ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) )`
46 18 29 37 45 syl3anc
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) )`
47 46 36 eqtrd
` |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V /\ ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) = V )`
48 47 rexlimdv3a
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> ( E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V -> ( ._|_ ` ( ._|_ ` X ) ) = V ) )`
49 15 48 mpd
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> ( ._|_ ` ( ._|_ ` X ) ) = V )`
50 simpr
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) = V )`
51 4 5 11 7 lshpne
` |-  ( ph -> X =/= V )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> X =/= V )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> V =/= X )`
` |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) =/= X )`
` |-  ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) =/= X <-> ( ._|_ ` ( ._|_ ` X ) ) = V ) )`