Metamath Proof Explorer

Theorem dochexmidlem4

Description: Lemma for dochexmid . (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 )
dochexmidlem4.pp 
|- ( ph -> p e. A )
dochexmidlem4.qq 
|- ( ph -> q e. A )
dochexmidlem4.z 
|- .0. = ( 0g ` U )
dochexmidlem4.m 
|- M = ( X .(+) p )
dochexmidlem4.xn 
|- ( ph -> X =/= { .0. } )
dochexmidlem4.pl 
|- ( ph -> q C_ ( ( ._|_ ` X ) i^i M ) )
Assertion dochexmidlem4 
|- ( ph -> p C_ ( X .(+) ( ._|_ ` 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 dochexmidlem4.pp 
 |-  ( ph -> p e. A )
12 dochexmidlem4.qq 
 |-  ( ph -> q e. A )
13 dochexmidlem4.z 
 |-  .0. = ( 0g ` U )
14 dochexmidlem4.m 
 |-  M = ( X .(+) p )
15 dochexmidlem4.xn 
 |-  ( ph -> X =/= { .0. } )
16 dochexmidlem4.pl 
 |-  ( ph -> q C_ ( ( ._|_ ` X ) i^i M ) )
17 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
18 5 8 17 11 lsatlssel 
 |-  ( ph -> p e. S )
19 inss2 
 |-  ( ( ._|_ ` X ) i^i M ) C_ M
20 16 19 sstrdi 
 |-  ( ph -> q C_ M )
21 20 14 sseqtrdi 
 |-  ( ph -> q C_ ( X .(+) p ) )
22 13 5 7 8 17 10 18 12 15 21 lsmsat 
 |-  ( ph -> E. r e. A ( r C_ X /\ q C_ ( r .(+) p ) ) )
23 9 3ad2ant1 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> ( K e. HL /\ W e. H ) )
24 10 3ad2ant1 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> X e. S )
25 11 3ad2ant1 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> p e. A )
26 12 3ad2ant1 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> q e. A )
27 simp2 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> r e. A )
28 inss1 
 |-  ( ( ._|_ ` X ) i^i M ) C_ ( ._|_ ` X )
29 16 28 sstrdi 
 |-  ( ph -> q C_ ( ._|_ ` X ) )
30 29 3ad2ant1 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> q C_ ( ._|_ ` X ) )
31 simp3l 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> r C_ X )
32 simp3r 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> q C_ ( r .(+) p ) )
33 1 2 3 4 5 6 7 8 23 24 25 26 27 30 31 32 dochexmidlem3 
 |-  ( ( ph /\ r e. A /\ ( r C_ X /\ q C_ ( r .(+) p ) ) ) -> p C_ ( X .(+) ( ._|_ ` X ) ) )
34 33 rexlimdv3a 
 |-  ( ph -> ( E. r e. A ( r C_ X /\ q C_ ( r .(+) p ) ) -> p C_ ( X .(+) ( ._|_ ` X ) ) ) )
35 22 34 mpd 
 |-  ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) )