Metamath Proof Explorer

Theorem dochexmidlem5

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 )
dochexmidlem5.pp 
|- ( ph -> p e. A )
dochexmidlem5.z 
|- .0. = ( 0g ` U )
dochexmidlem5.m 
|- M = ( X .(+) p )
dochexmidlem5.xn 
|- ( ph -> X =/= { .0. } )
dochexmidlem5.pl 
|- ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )
Assertion dochexmidlem5 
|- ( ph -> ( ( ._|_ ` X ) i^i M ) = { .0. } )

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 dochexmidlem5.pp 
 |-  ( ph -> p e. A )
12 dochexmidlem5.z 
 |-  .0. = ( 0g ` U )
13 dochexmidlem5.m 
 |-  M = ( X .(+) p )
14 dochexmidlem5.xn 
 |-  ( ph -> X =/= { .0. } )
15 dochexmidlem5.pl 
 |-  ( ph -> -. p C_ ( X .(+) ( ._|_ ` X ) ) )
16 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
17 16 adantr 
 |-  ( ( ph /\ ( ( ._|_ ` X ) i^i M ) =/= { .0. } ) -> U e. LMod )
18 4 5 lssss 
 |-  ( X e. S -> X C_ V )
19 10 18 syl 
 |-  ( ph -> X C_ V )
20 1 3 4 5 2 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. S )
21 9 19 20 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) e. S )
22 5 8 16 11 lsatlssel 
 |-  ( ph -> p e. S )
23 5 7 lsmcl 
 |-  ( ( U e. LMod /\ X e. S /\ p e. S ) -> ( X .(+) p ) e. S )
24 16 10 22 23 syl3anc 
 |-  ( ph -> ( X .(+) p ) e. S )
25 13 24 eqeltrid 
 |-  ( ph -> M e. S )
26 5 lssincl 
 |-  ( ( U e. LMod /\ ( ._|_ ` X ) e. S /\ M e. S ) -> ( ( ._|_ ` X ) i^i M ) e. S )
27 16 21 25 26 syl3anc 
 |-  ( ph -> ( ( ._|_ ` X ) i^i M ) e. S )
28 27 adantr 
 |-  ( ( ph /\ ( ( ._|_ ` X ) i^i M ) =/= { .0. } ) -> ( ( ._|_ ` X ) i^i M ) e. S )
29 simpr 
 |-  ( ( ph /\ ( ( ._|_ ` X ) i^i M ) =/= { .0. } ) -> ( ( ._|_ ` X ) i^i M ) =/= { .0. } )
30 5 12 8 17 28 29 lssatomic 
 |-  ( ( ph /\ ( ( ._|_ ` X ) i^i M ) =/= { .0. } ) -> E. q e. A q C_ ( ( ._|_ ` X ) i^i M ) )
31 30 ex 
 |-  ( ph -> ( ( ( ._|_ ` X ) i^i M ) =/= { .0. } -> E. q e. A q C_ ( ( ._|_ ` X ) i^i M ) ) )
32 9 3ad2ant1 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> ( K e. HL /\ W e. H ) )
33 10 3ad2ant1 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> X e. S )
34 11 3ad2ant1 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> p e. A )
35 simp2 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> q e. A )
36 14 3ad2ant1 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> X =/= { .0. } )
37 simp3 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> q C_ ( ( ._|_ ` X ) i^i M ) )
38 1 2 3 4 5 6 7 8 32 33 34 35 12 13 36 37 dochexmidlem4 
 |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> p C_ ( X .(+) ( ._|_ ` X ) ) )
39 38 rexlimdv3a 
 |-  ( ph -> ( E. q e. A q C_ ( ( ._|_ ` X ) i^i M ) -> p C_ ( X .(+) ( ._|_ ` X ) ) ) )
40 31 39 syld 
 |-  ( ph -> ( ( ( ._|_ ` X ) i^i M ) =/= { .0. } -> p C_ ( X .(+) ( ._|_ ` X ) ) ) )
41 40 necon1bd 
 |-  ( ph -> ( -. p C_ ( X .(+) ( ._|_ ` X ) ) -> ( ( ._|_ ` X ) i^i M ) = { .0. } ) )
42 15 41 mpd 
 |-  ( ph -> ( ( ._|_ ` X ) i^i M ) = { .0. } )