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 )
15 14 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> E. v e. V ( X ( LSSum ` U ) ( ( LSpan ` U ) ` { v } ) ) = V )
16 id 
 |-  ( ( ph /\ v e. V ) -> ( ph /\ v e. V ) )
17 16 adantlr 
 |-  ( ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) /\ v e. V ) -> ( ph /\ v e. V ) )
18 17 3adant3 
 |-  ( ( ( 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 ) ) )
24 23 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
25 24 3ad2ant1 
 |-  ( ( ( 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 )
34 33 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) =/= X ) -> ( ._|_ ` ( ._|_ ` X ) ) C_ V )
35 34 3ad2ant1 
 |-  ( ( ( 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 } ) ) )
38 6 adantr 
 |-  ( ( ph /\ v e. V ) -> ( K e. HL /\ W e. H ) )
39 1 3 38 dvhlvec 
 |-  ( ( ph /\ v e. V ) -> U e. LVec )
40 19 adantr 
 |-  ( ( 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 ) )
43 42 adantr 
 |-  ( ( 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 )
52 51 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> X =/= V )
53 52 necomd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> V =/= X )
54 50 53 eqnetrd 
 |-  ( ( ph /\ ( ._|_ ` ( ._|_ ` X ) ) = V ) -> ( ._|_ ` ( ._|_ ` X ) ) =/= X )
55 49 54 impbida 
 |-  ( ph -> ( ( ._|_ ` ( ._|_ ` X ) ) =/= X <-> ( ._|_ ` ( ._|_ ` X ) ) = V ) )