Metamath Proof Explorer


Theorem prdsdsval3

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-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 )
prdsdsval3.k
|- K = ( Base ` R )
prdsdsval3.e
|- E = ( ( dist ` R ) |` ( K X. K ) )
prdsdsval3.d
|- D = ( dist ` Y )
Assertion prdsdsval3
|- ( 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 prdsdsval3.k
 |-  K = ( Base ` R )
9 prdsdsval3.e
 |-  E = ( ( dist ` R ) |` ( K X. K ) )
10 prdsdsval3.d
 |-  D = ( dist ` Y )
11 eqid
 |-  ( dist ` R ) = ( dist ` R )
12 1 2 3 4 5 6 7 11 10 prdsdsval2
 |-  ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
13 eqidd
 |-  ( ph -> I = I )
14 1 2 3 4 5 8 6 prdsbascl
 |-  ( ph -> A. x e. I ( F ` x ) e. K )
15 1 2 3 4 5 8 7 prdsbascl
 |-  ( ph -> A. x e. I ( G ` x ) e. K )
16 9 oveqi
 |-  ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( ( dist ` R ) |` ( K X. K ) ) ( G ` x ) )
17 ovres
 |-  ( ( ( F ` x ) e. K /\ ( G ` x ) e. K ) -> ( ( F ` x ) ( ( dist ` R ) |` ( K X. K ) ) ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
18 16 17 eqtrid
 |-  ( ( ( F ` x ) e. K /\ ( G ` x ) e. K ) -> ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
19 18 ex
 |-  ( ( F ` x ) e. K -> ( ( G ` x ) e. K -> ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
20 19 ral2imi
 |-  ( A. x e. I ( F ` x ) e. K -> ( A. x e. I ( G ` x ) e. K -> A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
21 14 15 20 sylc
 |-  ( ph -> A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) )
22 mpteq12
 |-  ( ( I = I /\ A. x e. I ( ( F ` x ) E ( G ` x ) ) = ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) -> ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
23 13 21 22 syl2anc
 |-  ( ph -> ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
24 23 rneqd
 |-  ( ph -> ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) = ran ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) )
25 24 uneq1d
 |-  ( ph -> ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) = ( ran ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) )
26 25 supeq1d
 |-  ( ph -> sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` R ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
27 12 26 eqtr4d
 |-  ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) E ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )