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 )