Step |
Hyp |
Ref |
Expression |
1 |
|
mapdpglem.h |
|- H = ( LHyp ` K ) |
2 |
|
mapdpglem.m |
|- M = ( ( mapd ` K ) ` W ) |
3 |
|
mapdpglem.u |
|- U = ( ( DVecH ` K ) ` W ) |
4 |
|
mapdpglem.v |
|- V = ( Base ` U ) |
5 |
|
mapdpglem.s |
|- .- = ( -g ` U ) |
6 |
|
mapdpglem.n |
|- N = ( LSpan ` U ) |
7 |
|
mapdpglem.c |
|- C = ( ( LCDual ` K ) ` W ) |
8 |
|
mapdpglem.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
9 |
|
mapdpglem.x |
|- ( ph -> X e. V ) |
10 |
|
mapdpglem.y |
|- ( ph -> Y e. V ) |
11 |
|
mapdpglem1.p |
|- .(+) = ( LSSum ` C ) |
12 |
|
mapdpglem2.j |
|- J = ( LSpan ` C ) |
13 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
14 |
1 3 8
|
dvhlmod |
|- ( ph -> U e. LMod ) |
15 |
4 5
|
lmodvsubcl |
|- ( ( U e. LMod /\ X e. V /\ Y e. V ) -> ( X .- Y ) e. V ) |
16 |
14 9 10 15
|
syl3anc |
|- ( ph -> ( X .- Y ) e. V ) |
17 |
1 2 3 4 6 7 13 12 8 16
|
mapdspex |
|- ( ph -> E. t e. ( Base ` C ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |
18 |
1 7 8
|
lcdlmod |
|- ( ph -> C e. LMod ) |
19 |
13 12
|
lspsnid |
|- ( ( C e. LMod /\ t e. ( Base ` C ) ) -> t e. ( J ` { t } ) ) |
20 |
18 19
|
sylan |
|- ( ( ph /\ t e. ( Base ` C ) ) -> t e. ( J ` { t } ) ) |
21 |
20
|
adantrr |
|- ( ( ph /\ ( t e. ( Base ` C ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) ) -> t e. ( J ` { t } ) ) |
22 |
|
simprr |
|- ( ( ph /\ ( t e. ( Base ` C ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) ) -> ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |
23 |
21 22
|
eleqtrrd |
|- ( ( ph /\ ( t e. ( Base ` C ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) ) -> t e. ( M ` ( N ` { ( X .- Y ) } ) ) ) |
24 |
17 23 22
|
reximssdv |
|- ( ph -> E. t e. ( M ` ( N ` { ( X .- Y ) } ) ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |
25 |
1 2 3 4 5 6 7 8 9 10 11
|
mapdpglem1 |
|- ( ph -> ( M ` ( N ` { ( X .- Y ) } ) ) C_ ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ) |
26 |
25
|
sseld |
|- ( ph -> ( t e. ( M ` ( N ` { ( X .- Y ) } ) ) -> t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ) ) |
27 |
26
|
anim1d |
|- ( ph -> ( ( t e. ( M ` ( N ` { ( X .- Y ) } ) ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) -> ( t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) ) ) |
28 |
27
|
reximdv2 |
|- ( ph -> ( E. t e. ( M ` ( N ` { ( X .- Y ) } ) ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) -> E. t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) ) |
29 |
24 28
|
mpd |
|- ( ph -> E. t e. ( ( M ` ( N ` { X } ) ) .(+) ( M ` ( N ` { Y } ) ) ) ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { t } ) ) |