| 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 ) |