Metamath Proof Explorer

Theorem dochexmidlem6

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 )
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 dochexmidlem6 
|- ( 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 2 3 4 5 6 7 8 9 10 11 12 13 14 16 dochexmidlem5 
 |-  ( ph -> ( ( ._|_ ` X ) i^i M ) = { .0. } )
18 17 fveq2d 
 |-  ( ph -> ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) = ( ._|_ ` { .0. } ) )
19 1 3 2 4 12 doch0 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { .0. } ) = V )
20 9 19 syl 
 |-  ( ph -> ( ._|_ ` { .0. } ) = V )
21 18 20 eqtrd 
 |-  ( ph -> ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) = V )
22 21 ineq1d 
 |-  ( ph -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) i^i M ) = ( V i^i M ) )
23 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
24 4 5 lssss 
 |-  ( X e. S -> X C_ V )
25 10 24 syl 
 |-  ( ph -> X C_ V )
26 1 3 4 2 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) C_ V )
27 9 25 26 syl2anc 
 |-  ( ph -> ( ._|_ ` X ) C_ V )
28 1 23 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) C_ V ) -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
29 9 27 28 syl2anc 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` X ) ) e. ran ( ( DIsoH ` K ) ` W ) )
30 15 29 eqeltrrd 
 |-  ( ph -> X e. ran ( ( DIsoH ` K ) ` W ) )
31 1 23 3 7 8 9 30 11 dihsmatrn 
 |-  ( ph -> ( X .(+) p ) e. ran ( ( DIsoH ` K ) ` W ) )
32 13 31 eqeltrid 
 |-  ( ph -> M e. ran ( ( DIsoH ` K ) ` W ) )
33 1 3 23 5 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ M e. ran ( ( DIsoH ` K ) ` W ) ) -> M e. S )
34 9 32 33 syl2anc 
 |-  ( ph -> M e. S )
35 1 3 9 dvhlmod 
 |-  ( ph -> U e. LMod )
36 5 8 35 11 lsatlssel 
 |-  ( ph -> p e. S )
37 5 7 lsmcl 
 |-  ( ( U e. LMod /\ X e. S /\ p e. S ) -> ( X .(+) p ) e. S )
38 35 10 36 37 syl3anc 
 |-  ( ph -> ( X .(+) p ) e. S )
39 4 5 lssss 
 |-  ( ( X .(+) p ) e. S -> ( X .(+) p ) C_ V )
40 38 39 syl 
 |-  ( ph -> ( X .(+) p ) C_ V )
41 13 40 eqsstrid 
 |-  ( ph -> M C_ V )
42 1 23 3 4 2 9 41 dochoccl 
 |-  ( ph -> ( M e. ran ( ( DIsoH ` K ) ` W ) <-> ( ._|_ ` ( ._|_ ` M ) ) = M ) )
43 32 42 mpbid 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` M ) ) = M )
44 5 lsssssubg 
 |-  ( U e. LMod -> S C_ ( SubGrp ` U ) )
45 35 44 syl 
 |-  ( ph -> S C_ ( SubGrp ` U ) )
46 45 10 sseldd 
 |-  ( ph -> X e. ( SubGrp ` U ) )
47 45 36 sseldd 
 |-  ( ph -> p e. ( SubGrp ` U ) )
48 7 lsmub1 
 |-  ( ( X e. ( SubGrp ` U ) /\ p e. ( SubGrp ` U ) ) -> X C_ ( X .(+) p ) )
49 46 47 48 syl2anc 
 |-  ( ph -> X C_ ( X .(+) p ) )
50 49 13 sseqtrrdi 
 |-  ( ph -> X C_ M )
51 1 3 5 2 9 10 34 43 50 dihoml4 
 |-  ( ph -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i M ) ) i^i M ) = ( ._|_ ` ( ._|_ ` X ) ) )
52 sseqin2 
 |-  ( M C_ V <-> ( V i^i M ) = M )
53 41 52 sylib 
 |-  ( ph -> ( V i^i M ) = M )
54 22 51 53 3eqtr3rd 
 |-  ( ph -> M = ( ._|_ ` ( ._|_ ` X ) ) )
55 54 15 eqtrd 
 |-  ( ph -> M = X )