| 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 |
|
dochexmidlem2.pp |
|- ( ph -> p e. A ) |
| 12 |
|
dochexmidlem2.qq |
|- ( ph -> q e. A ) |
| 13 |
|
dochexmidlem2.rr |
|- ( ph -> r e. A ) |
| 14 |
|
dochexmidlem2.ql |
|- ( ph -> q C_ ( ._|_ ` X ) ) |
| 15 |
|
dochexmidlem2.rl |
|- ( ph -> r C_ X ) |
| 16 |
|
dochexmidlem2.pl |
|- ( ph -> p C_ ( r .(+) q ) ) |
| 17 |
1 3 9
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 18 |
5
|
lsssssubg |
|- ( U e. LMod -> S C_ ( SubGrp ` U ) ) |
| 19 |
17 18
|
syl |
|- ( ph -> S C_ ( SubGrp ` U ) ) |
| 20 |
19 10
|
sseldd |
|- ( ph -> X e. ( SubGrp ` U ) ) |
| 21 |
4 5
|
lssss |
|- ( X e. S -> X C_ V ) |
| 22 |
10 21
|
syl |
|- ( ph -> X C_ V ) |
| 23 |
1 3 4 5 2
|
dochlss |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. S ) |
| 24 |
9 22 23
|
syl2anc |
|- ( ph -> ( ._|_ ` X ) e. S ) |
| 25 |
19 24
|
sseldd |
|- ( ph -> ( ._|_ ` X ) e. ( SubGrp ` U ) ) |
| 26 |
7
|
lsmless12 |
|- ( ( ( X e. ( SubGrp ` U ) /\ ( ._|_ ` X ) e. ( SubGrp ` U ) ) /\ ( r C_ X /\ q C_ ( ._|_ ` X ) ) ) -> ( r .(+) q ) C_ ( X .(+) ( ._|_ ` X ) ) ) |
| 27 |
20 25 15 14 26
|
syl22anc |
|- ( ph -> ( r .(+) q ) C_ ( X .(+) ( ._|_ ` X ) ) ) |
| 28 |
16 27
|
sstrd |
|- ( ph -> p C_ ( X .(+) ( ._|_ ` X ) ) ) |