Metamath Proof Explorer

Theorem prdsdsval2

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsbasmpt2.y 
|- Y = ( S Xs_ ( x e. I |-> R ) )
prdsbasmpt2.b 
|- B = ( Base ` Y )
prdsbasmpt2.s 
|- ( ph -> S e. V )
prdsbasmpt2.i 
|- ( ph -> I e. W )
prdsbasmpt2.r 
|- ( ph -> A. x e. I R e. X )
prdsdsval2.f 
|- ( ph -> F e. B )
prdsdsval2.g 
|- ( ph -> G e. B )
prdsdsval2.e 
|- E = ( dist ` R )
prdsdsval2.d 
|- D = ( dist ` Y )
Assertion prdsdsval2 
|- ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )

Proof

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 syl5eq 
 |-  ( 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* , < ) )