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