Step |
Hyp |
Ref |
Expression |
1 |
|
prdsbasmpt2.y |
|- Y = ( S Xs_ ( x e. I |-> R ) ) |
2 |
|
prdsbasmpt2.b |
|- B = ( Base ` Y ) |
3 |
|
prdsbasmpt2.s |
|- ( ph -> S e. V ) |
4 |
|
prdsbasmpt2.i |
|- ( ph -> I e. W ) |
5 |
|
prdsbasmpt2.r |
|- ( ph -> A. x e. I R e. X ) |
6 |
|
prdsdsval2.f |
|- ( ph -> F e. B ) |
7 |
|
prdsdsval2.g |
|- ( ph -> G e. B ) |
8 |
|
prdsdsval2.e |
|- E = ( dist ` R ) |
9 |
|
prdsdsval2.d |
|- D = ( dist ` Y ) |
10 |
|
eqid |
|- ( x e. I |-> R ) = ( x e. I |-> R ) |
11 |
10
|
fnmpt |
|- ( A. x e. I R e. X -> ( x e. I |-> R ) Fn I ) |
12 |
5 11
|
syl |
|- ( ph -> ( x e. I |-> R ) Fn I ) |
13 |
1 2 3 4 12 6 7 9
|
prdsdsval |
|- ( ph -> ( F D G ) = sup ( ( ran ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) u. { 0 } ) , RR* , < ) ) |
14 |
|
nfcv |
|- F/_ x ( F ` y ) |
15 |
|
nfcv |
|- F/_ x dist |
16 |
|
nffvmpt1 |
|- F/_ x ( ( x e. I |-> R ) ` y ) |
17 |
15 16
|
nffv |
|- F/_ x ( dist ` ( ( x e. I |-> R ) ` y ) ) |
18 |
|
nfcv |
|- F/_ x ( G ` y ) |
19 |
14 17 18
|
nfov |
|- F/_ x ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) |
20 |
|
nfcv |
|- F/_ y ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) |
21 |
|
2fveq3 |
|- ( y = x -> ( dist ` ( ( x e. I |-> R ) ` y ) ) = ( dist ` ( ( x e. I |-> R ) ` x ) ) ) |
22 |
|
fveq2 |
|- ( y = x -> ( F ` y ) = ( F ` x ) ) |
23 |
|
fveq2 |
|- ( y = x -> ( G ` y ) = ( G ` x ) ) |
24 |
21 22 23
|
oveq123d |
|- ( y = x -> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) = ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) ) |
25 |
19 20 24
|
cbvmpt |
|- ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) = ( x e. I |-> ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) ) |
26 |
|
eqidd |
|- ( ph -> I = I ) |
27 |
10
|
fvmpt2 |
|- ( ( x e. I /\ R e. X ) -> ( ( x e. I |-> R ) ` x ) = R ) |
28 |
27
|
fveq2d |
|- ( ( x e. I /\ R e. X ) -> ( dist ` ( ( x e. I |-> R ) ` x ) ) = ( dist ` R ) ) |
29 |
28 8
|
eqtr4di |
|- ( ( x e. I /\ R e. X ) -> ( dist ` ( ( x e. I |-> R ) ` x ) ) = E ) |
30 |
29
|
oveqd |
|- ( ( x e. I /\ R e. X ) -> ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) = ( ( F ` x ) E ( G ` x ) ) ) |
31 |
30
|
ralimiaa |
|- ( A. x e. I R e. X -> A. x e. I ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) = ( ( F ` x ) E ( G ` x ) ) ) |
32 |
5 31
|
syl |
|- ( ph -> A. x e. I ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) = ( ( F ` x ) E ( G ` x ) ) ) |
33 |
|
mpteq12 |
|- ( ( I = I /\ A. x e. I ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) = ( ( F ` x ) E ( G ` x ) ) ) -> ( x e. I |-> ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) ) |
34 |
26 32 33
|
syl2anc |
|- ( ph -> ( x e. I |-> ( ( F ` x ) ( dist ` ( ( x e. I |-> R ) ` x ) ) ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) ) |
35 |
25 34
|
eqtrid |
|- ( ph -> ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) = ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) ) |
36 |
35
|
rneqd |
|- ( ph -> ran ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) = ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) ) |
37 |
36
|
uneq1d |
|- ( ph -> ( ran ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) u. { 0 } ) = ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) ) |
38 |
37
|
supeq1d |
|- ( ph -> sup ( ( ran ( y e. I |-> ( ( F ` y ) ( dist ` ( ( x e. I |-> R ) ` y ) ) ( G ` y ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) ) |
39 |
13 38
|
eqtrd |
|- ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) ) |