Metamath Proof Explorer


Theorem prdsdsval

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

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

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y
 |-  Y = ( S Xs_ R )
2 prdsbasmpt.b
 |-  B = ( Base ` Y )
3 prdsbasmpt.s
 |-  ( ph -> S e. V )
4 prdsbasmpt.i
 |-  ( ph -> I e. W )
5 prdsbasmpt.r
 |-  ( ph -> R Fn I )
6 prdsplusgval.f
 |-  ( ph -> F e. B )
7 prdsplusgval.g
 |-  ( ph -> G e. B )
8 prdsdsval.d
 |-  D = ( dist ` Y )
9 fnex
 |-  ( ( R Fn I /\ I e. W ) -> R e. _V )
10 5 4 9 syl2anc
 |-  ( ph -> R e. _V )
11 fndm
 |-  ( R Fn I -> dom R = I )
12 5 11 syl
 |-  ( ph -> dom R = I )
13 1 3 10 2 12 8 prdsds
 |-  ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
14 fveq1
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
15 fveq1
 |-  ( g = G -> ( g ` x ) = ( G ` x ) )
16 14 15 oveqan12d
 |-  ( ( f = F /\ g = G ) -> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) = ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) )
17 16 adantl
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) = ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) )
18 17 mpteq2dv
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) )
19 18 rneqd
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) = ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) )
20 19 uneq1d
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) = ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) )
21 20 supeq1d
 |-  ( ( ph /\ ( f = F /\ g = G ) ) -> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )
22 xrltso
 |-  < Or RR*
23 22 supex
 |-  sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) e. _V
24 23 a1i
 |-  ( ph -> sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) e. _V )
25 13 21 6 7 24 ovmpod
 |-  ( ph -> ( F D G ) = sup ( ( ran ( x e. I |-> ( ( F ` x ) ( dist ` ( R ` x ) ) ( G ` x ) ) ) u. { 0 } ) , RR* , < ) )