Metamath Proof Explorer

Theorem dochexmidlem8

Description: Lemma for dochexmid . The contradiction of dochexmidlem6 and dochexmidlem7 shows that there can be no atom p that is not in X + ( ._|_X ) , which is therefore the whole atom space. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dochexmidlem1.h 
|- H = ( LHyp ` K )
dochexmidlem1.o 
|- ._|_ = ( ( ocH ` K ) ` W )
dochexmidlem1.u 
|- U = ( ( DVecH ` K ) ` W )
dochexmidlem1.v 
|- V = ( Base ` U )
dochexmidlem1.s 
|- S = ( LSubSp ` U )
dochexmidlem1.n 
|- N = ( LSpan ` U )
dochexmidlem1.p 
|- .(+) = ( LSSum ` U )
dochexmidlem1.a 
|- A = ( LSAtoms ` U )
dochexmidlem1.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochexmidlem1.x 
|- ( ph -> X e. S )
dochexmidlem8.z 
|- .0. = ( 0g ` U )
dochexmidlem8.xn 
|- ( ph -> X =/= { .0. } )
dochexmidlem8.c 
|- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Assertion dochexmidlem8 
|- ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )

Proof

Step Hyp Ref Expression
1 dochexmidlem1.h 
 |-  H = ( LHyp ` K )
2 dochexmidlem1.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 dochexmidlem1.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 dochexmidlem1.v 
 |-  V = ( Base ` U )
5 dochexmidlem1.s 
 |-  S = ( LSubSp ` U )
6 dochexmidlem1.n 
 |-  N = ( LSpan ` U )
7 dochexmidlem1.p 
 |-  .(+) = ( LSSum ` U )
8 dochexmidlem1.a 
 |-  A = ( LSAtoms ` U )
9 dochexmidlem1.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 dochexmidlem1.x 
 |-  ( ph -> X e. S )
11 dochexmidlem8.z 
 |-  .0. = ( 0g ` U )
12 dochexmidlem8.xn 
 |-  ( ph -> X =/= { .0. } )
13 dochexmidlem8.c 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
14 nonconne 
 |-  -. ( X = X /\ X =/= X )
15 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
16 4 5 lssss 
 |-  ( X e. S -> X C_ V )
17 10 16 syl 
 |-  ( ph -> X C_ V )
18 1 3 4 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. S )
19 9 17 18 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. S )
20 5 7 lsmcl 
 |-  ( ( U e. LMod /\ X e. S /\ ( ._|_ ` X ) e. S ) -> ( X .(+) ( ._|_ ` X ) ) e. S )
21 15 10 19 20 syl3anc 
 |-  ( ph -> ( X .(+) ( ._|_ ` X ) ) e. S )
22 4 5 lssss 
 |-  ( ( X .(+) ( ._|_ ` X ) ) e. S -> ( X .(+) ( ._|_ ` X ) ) C_ V )
23 21 22 syl 
 |-  ( ph -> ( X .(+) ( ._|_ ` X ) ) C_ V )
24 15 adantr 
 |-  ( ( ph /\ ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) ) -> U e. LMod )
25 21 adantr 
 |-  ( ( ph /\ ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) ) -> ( X .(+) ( ._|_ ` X ) ) e. S )
26 4 5 lss1 
 |-  ( U e. LMod -> V e. S )
27 15 26 syl 
 |-  ( ph -> V e. S )
28 27 adantr 
 |-  ( ( ph /\ ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) ) -> V e. S )
29 df-pss 
 |-  ( ( X .(+) ( ._|_ ` X ) ) C. V <-> ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) )
30 29 biimpri 
 |-  ( ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) -> ( X .(+) ( ._|_ ` X ) ) C. V )
31 30 adantl 
 |-  ( ( ph /\ ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) ) -> ( X .(+) ( ._|_ ` X ) ) C. V )
32 5 8 24 25 28 31 lpssat 
 |-  ( ( ph /\ ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) ) -> E. p e. A ( p C_ V /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) )
33 32 ex 
 |-  ( ph -> ( ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) -> E. p e. A ( p C_ V /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) ) )
34 9 3ad2ant1 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( K e. HL /\ W e. H ) )
35 10 3ad2ant1 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> X e. S )
36 simp2 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> p e. A )
37 eqid 
 |-  ( X .(+) p ) = ( X .(+) p )
38 12 3ad2ant1 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> X =/= { .0. } )
39 13 3ad2ant1 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
40 simp3 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )
41 1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40 dochexmidlem6 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( X .(+) p ) = X )
42 1 2 3 4 5 6 7 8 34 35 36 11 37 38 39 40 dochexmidlem7 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( X .(+) p ) =/= X )
43 41 42 pm2.21ddne 
 |-  ( ( ph /\ p e. A /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( X = X /\ X =/= X ) )
44 43 3adant3l 
 |-  ( ( ph /\ p e. A /\ ( p C_ V /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) ) -> ( X = X /\ X =/= X ) )
45 44 rexlimdv3a 
 |-  ( ph -> ( E. p e. A ( p C_ V /\ -. p C_ ( X .(+) ( ._|_ ` X ) ) ) -> ( X = X /\ X =/= X ) ) )
46 33 45 syld 
 |-  ( ph -> ( ( ( X .(+) ( ._|_ ` X ) ) C_ V /\ ( X .(+) ( ._|_ ` X ) ) =/= V ) -> ( X = X /\ X =/= X ) ) )
47 23 46 mpand 
 |-  ( ph -> ( ( X .(+) ( ._|_ ` X ) ) =/= V -> ( X = X /\ X =/= X ) ) )
48 47 necon1bd 
 |-  ( ph -> ( -. ( X = X /\ X =/= X ) -> ( X .(+) ( ._|_ ` X ) ) = V ) )
49 14 48 mpi 
 |-  ( ph -> ( X .(+) ( ._|_ ` X ) ) = V )