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