Step |
Hyp |
Ref |
Expression |
1 |
|
mapdh.q |
|- Q = ( 0g ` C ) |
2 |
|
mapdh.i |
|- I = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) ) |
3 |
|
mapdh.h |
|- H = ( LHyp ` K ) |
4 |
|
mapdh.m |
|- M = ( ( mapd ` K ) ` W ) |
5 |
|
mapdh.u |
|- U = ( ( DVecH ` K ) ` W ) |
6 |
|
mapdh.v |
|- V = ( Base ` U ) |
7 |
|
mapdh.s |
|- .- = ( -g ` U ) |
8 |
|
mapdhc.o |
|- .0. = ( 0g ` U ) |
9 |
|
mapdh.n |
|- N = ( LSpan ` U ) |
10 |
|
mapdh.c |
|- C = ( ( LCDual ` K ) ` W ) |
11 |
|
mapdh.d |
|- D = ( Base ` C ) |
12 |
|
mapdh.r |
|- R = ( -g ` C ) |
13 |
|
mapdh.j |
|- J = ( LSpan ` C ) |
14 |
|
mapdh.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
15 |
|
mapdhc.f |
|- ( ph -> F e. D ) |
16 |
|
mapdh.mn |
|- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
17 |
|
mapdhcl.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
18 |
|
mapdhc.y |
|- ( ph -> Y e. V ) |
19 |
|
mapdh.ne |
|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
20 |
|
oteq3 |
|- ( Y = .0. -> <. X , F , Y >. = <. X , F , .0. >. ) |
21 |
20
|
fveq2d |
|- ( Y = .0. -> ( I ` <. X , F , Y >. ) = ( I ` <. X , F , .0. >. ) ) |
22 |
21
|
eleq1d |
|- ( Y = .0. -> ( ( I ` <. X , F , Y >. ) e. D <-> ( I ` <. X , F , .0. >. ) e. D ) ) |
23 |
17
|
adantr |
|- ( ( ph /\ Y =/= .0. ) -> X e. ( V \ { .0. } ) ) |
24 |
15
|
adantr |
|- ( ( ph /\ Y =/= .0. ) -> F e. D ) |
25 |
18
|
anim1i |
|- ( ( ph /\ Y =/= .0. ) -> ( Y e. V /\ Y =/= .0. ) ) |
26 |
|
eldifsn |
|- ( Y e. ( V \ { .0. } ) <-> ( Y e. V /\ Y =/= .0. ) ) |
27 |
25 26
|
sylibr |
|- ( ( ph /\ Y =/= .0. ) -> Y e. ( V \ { .0. } ) ) |
28 |
1 2 23 24 27
|
mapdhval2 |
|- ( ( ph /\ Y =/= .0. ) -> ( I ` <. X , F , Y >. ) = ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) ) |
29 |
14
|
adantr |
|- ( ( ph /\ Y =/= .0. ) -> ( K e. HL /\ W e. H ) ) |
30 |
19
|
adantr |
|- ( ( ph /\ Y =/= .0. ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) |
31 |
16
|
adantr |
|- ( ( ph /\ Y =/= .0. ) -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) ) |
32 |
3 4 5 6 7 8 9 10 11 12 13 29 23 27 24 30 31
|
mapdpg |
|- ( ( ph /\ Y =/= .0. ) -> E! h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) |
33 |
|
riotacl |
|- ( E! h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) -> ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) e. D ) |
34 |
32 33
|
syl |
|- ( ( ph /\ Y =/= .0. ) -> ( iota_ h e. D ( ( M ` ( N ` { Y } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( X .- Y ) } ) ) = ( J ` { ( F R h ) } ) ) ) e. D ) |
35 |
28 34
|
eqeltrd |
|- ( ( ph /\ Y =/= .0. ) -> ( I ` <. X , F , Y >. ) e. D ) |
36 |
1 2 8 17 15
|
mapdhval0 |
|- ( ph -> ( I ` <. X , F , .0. >. ) = Q ) |
37 |
3 10 11 1 14
|
lcd0vcl |
|- ( ph -> Q e. D ) |
38 |
36 37
|
eqeltrd |
|- ( ph -> ( I ` <. X , F , .0. >. ) e. D ) |
39 |
22 35 38
|
pm2.61ne |
|- ( ph -> ( I ` <. X , F , Y >. ) e. D ) |