Step |
Hyp |
Ref |
Expression |
1 |
|
hgmaprnlem1.h |
|- H = ( LHyp ` K ) |
2 |
|
hgmaprnlem1.u |
|- U = ( ( DVecH ` K ) ` W ) |
3 |
|
hgmaprnlem1.v |
|- V = ( Base ` U ) |
4 |
|
hgmaprnlem1.r |
|- R = ( Scalar ` U ) |
5 |
|
hgmaprnlem1.b |
|- B = ( Base ` R ) |
6 |
|
hgmaprnlem1.t |
|- .x. = ( .s ` U ) |
7 |
|
hgmaprnlem1.o |
|- .0. = ( 0g ` U ) |
8 |
|
hgmaprnlem1.c |
|- C = ( ( LCDual ` K ) ` W ) |
9 |
|
hgmaprnlem1.d |
|- D = ( Base ` C ) |
10 |
|
hgmaprnlem1.p |
|- P = ( Scalar ` C ) |
11 |
|
hgmaprnlem1.a |
|- A = ( Base ` P ) |
12 |
|
hgmaprnlem1.e |
|- .xb = ( .s ` C ) |
13 |
|
hgmaprnlem1.q |
|- Q = ( 0g ` C ) |
14 |
|
hgmaprnlem1.s |
|- S = ( ( HDMap ` K ) ` W ) |
15 |
|
hgmaprnlem1.g |
|- G = ( ( HGMap ` K ) ` W ) |
16 |
|
hgmaprnlem1.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
17 |
|
hgmaprnlem1.z |
|- ( ph -> z e. A ) |
18 |
|
hgmaprnlem1.t2 |
|- ( ph -> t e. ( V \ { .0. } ) ) |
19 |
|
hgmaprnlem1.s2 |
|- ( ph -> s e. V ) |
20 |
|
hgmaprnlem1.sz |
|- ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) ) |
21 |
|
hgmaprnlem1.m |
|- M = ( ( mapd ` K ) ` W ) |
22 |
|
hgmaprnlem1.n |
|- N = ( LSpan ` U ) |
23 |
|
hgmaprnlem1.l |
|- L = ( LSpan ` C ) |
24 |
1 8 16
|
lcdlmod |
|- ( ph -> C e. LMod ) |
25 |
18
|
eldifad |
|- ( ph -> t e. V ) |
26 |
1 2 3 8 9 14 16 25
|
hdmapcl |
|- ( ph -> ( S ` t ) e. D ) |
27 |
10 11 9 12 23
|
lspsnvsi |
|- ( ( C e. LMod /\ z e. A /\ ( S ` t ) e. D ) -> ( L ` { ( z .xb ( S ` t ) ) } ) C_ ( L ` { ( S ` t ) } ) ) |
28 |
24 17 26 27
|
syl3anc |
|- ( ph -> ( L ` { ( z .xb ( S ` t ) ) } ) C_ ( L ` { ( S ` t ) } ) ) |
29 |
1 2 3 22 8 23 21 14 16 19
|
hdmap10 |
|- ( ph -> ( M ` ( N ` { s } ) ) = ( L ` { ( S ` s ) } ) ) |
30 |
20
|
sneqd |
|- ( ph -> { ( S ` s ) } = { ( z .xb ( S ` t ) ) } ) |
31 |
30
|
fveq2d |
|- ( ph -> ( L ` { ( S ` s ) } ) = ( L ` { ( z .xb ( S ` t ) ) } ) ) |
32 |
29 31
|
eqtrd |
|- ( ph -> ( M ` ( N ` { s } ) ) = ( L ` { ( z .xb ( S ` t ) ) } ) ) |
33 |
1 2 3 22 8 23 21 14 16 25
|
hdmap10 |
|- ( ph -> ( M ` ( N ` { t } ) ) = ( L ` { ( S ` t ) } ) ) |
34 |
28 32 33
|
3sstr4d |
|- ( ph -> ( M ` ( N ` { s } ) ) C_ ( M ` ( N ` { t } ) ) ) |
35 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
36 |
1 2 16
|
dvhlmod |
|- ( ph -> U e. LMod ) |
37 |
3 35 22
|
lspsncl |
|- ( ( U e. LMod /\ s e. V ) -> ( N ` { s } ) e. ( LSubSp ` U ) ) |
38 |
36 19 37
|
syl2anc |
|- ( ph -> ( N ` { s } ) e. ( LSubSp ` U ) ) |
39 |
3 35 22
|
lspsncl |
|- ( ( U e. LMod /\ t e. V ) -> ( N ` { t } ) e. ( LSubSp ` U ) ) |
40 |
36 25 39
|
syl2anc |
|- ( ph -> ( N ` { t } ) e. ( LSubSp ` U ) ) |
41 |
1 2 35 21 16 38 40
|
mapdord |
|- ( ph -> ( ( M ` ( N ` { s } ) ) C_ ( M ` ( N ` { t } ) ) <-> ( N ` { s } ) C_ ( N ` { t } ) ) ) |
42 |
34 41
|
mpbid |
|- ( ph -> ( N ` { s } ) C_ ( N ` { t } ) ) |