This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochexmidlem7

Description: Lemma for dochexmid . Contradict dochexmidlem6 . (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 )
dochexmidlem6.pp 
|- ( ph -> p e. A )
dochexmidlem6.z 
|- .0. = ( 0g ` U )
dochexmidlem6.m 
|- M = ( X .(+) p )
dochexmidlem6.xn 
|- ( ph -> X =/= { .0. } )
dochexmidlem6.c 
|- ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
dochexmidlem6.pl 
|- ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )
Assertion dochexmidlem7 
|- ( ph -> M =/= X )

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 dochexmidlem6.pp 
 |-  ( ph -> p e. A )
12 dochexmidlem6.z 
 |-  .0. = ( 0g ` U )
13 dochexmidlem6.m 
 |-  M = ( X .(+) p )
14 dochexmidlem6.xn 
 |-  ( ph -> X =/= { .0. } )
15 dochexmidlem6.c 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) = X )
16 dochexmidlem6.pl 
 |-  ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )
17 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
18 5 lsssssubg 
 |-  ( U e. LMod -> S C_ ( SubGrp ` U ) )
19 17 18 syl 
 |-  ( ph -> S C_ ( SubGrp ` U ) )
20 19 10 sseldd 
 |-  ( ph -> X e. ( SubGrp ` U ) )
21 5 8 17 11 lsatlssel 
 |-  ( ph -> p e. S )
22 19 21 sseldd 
 |-  ( ph -> p e. ( SubGrp ` U ) )
23 7 lsmub2 
 |-  ( ( X e. ( SubGrp ` U ) /\ p e. ( SubGrp ` U ) ) -> p C_ ( X .(+) p ) )
24 20 22 23 syl2anc 
 |-  ( ph -> p C_ ( X .(+) p ) )
25 24 13 sseqtrrdi 
 |-  ( ph -> p C_ M )
26 4 5 lssss 
 |-  ( X e. S -> X C_ V )
27 10 26 syl 
 |-  ( ph -> X C_ V )
28 1 3 4 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. S )
29 9 27 28 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. S )
30 19 29 sseldd 
 |-  ( ph -> ( ._|_ ` X ) e. ( SubGrp ` U ) )
31 7 lsmub1 
 |-  ( ( X e. ( SubGrp ` U ) /\ ( ._|_ ` X ) e. ( SubGrp ` U ) ) -> X C_ ( X .(+) ( ._|_ ` X ) ) )
32 20 30 31 syl2anc 
 |-  ( ph -> X C_ ( X .(+) ( ._|_ ` X ) ) )
33 sstr2 
 |-  ( p C_ X -> ( X C_ ( X .(+) ( ._|_ ` X ) ) -> p C_ ( X .(+) ( ._|_ ` X ) ) ) )
34 32 33 syl5com 
 |-  ( ph -> ( p C_ X -> p C_ ( X .(+) ( ._|_ ` X ) ) ) )
35 16 34 mtod 
 |-  ( ph -> -. p C_ X )
36 sseq2 
 |-  ( M = X -> ( p C_ M <-> p C_ X ) )
37 36 biimpcd 
 |-  ( p C_ M -> ( M = X -> p C_ X ) )
38 37 necon3bd 
 |-  ( p C_ M -> ( -. p C_ X -> M =/= X ) )
39 25 35 38 sylc 
 |-  ( ph -> M =/= X )