# 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 )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> ( K e. HL /\ W e. H ) )`
` |-  ( ( ph /\ q e. A /\ q C_ ( ( ._|_ ` X ) i^i M ) ) -> X e. S )`
` |-  ( ( 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 )`
` |-  ( ( 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. } )`