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 𝑠 x I R
prdsbasmpt2.b B = Base Y
prdsbasmpt2.s φ S V
prdsbasmpt2.i φ I W
prdsbasmpt2.r φ x I R X
prdsdsval2.f φ F B
prdsdsval2.g φ G B
prdsdsval2.e E = dist R
prdsdsval2.d D = dist Y
Assertion prdsdsval2 φ F D G = sup ran x I F x E G x 0 * <

Proof

Step Hyp Ref Expression
1 prdsbasmpt2.y Y = S 𝑠 x I R
2 prdsbasmpt2.b B = Base Y
3 prdsbasmpt2.s φ S V
4 prdsbasmpt2.i φ I W
5 prdsbasmpt2.r φ x I R X
6 prdsdsval2.f φ F B
7 prdsdsval2.g φ G B
8 prdsdsval2.e E = dist R
9 prdsdsval2.d D = dist Y
10 eqid x I R = x I R
11 10 fnmpt x I R X x I R Fn I
12 5 11 syl φ x I R Fn I
13 1 2 3 4 12 6 7 9 prdsdsval φ F D G = sup ran y I F y dist x I R y G y 0 * <
14 nfcv _ x F y
15 nfcv _ x dist
16 nffvmpt1 _ x x I R y
17 15 16 nffv _ x dist x I R y
18 nfcv _ x G y
19 14 17 18 nfov _ x F y dist x I R y G y
20 nfcv _ y F x dist x I R x G x
21 2fveq3 y = x dist x I R y = dist x 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 I R y G y = F x dist x I R x G x
25 19 20 24 cbvmpt y I F y dist x I R y G y = x I F x dist x I R x G x
26 eqidd φ I = I
27 10 fvmpt2 x I R X x I R x = R
28 27 fveq2d x I R X dist x I R x = dist R
29 28 8 eqtr4di x I R X dist x I R x = E
30 29 oveqd x I R X F x dist x I R x G x = F x E G x
31 30 ralimiaa x I R X x I F x dist x I R x G x = F x E G x
32 5 31 syl φ x I F x dist x I R x G x = F x E G x
33 mpteq12 I = I x I F x dist x I R x G x = F x E G x x I F x dist x I R x G x = x I F x E G x
34 26 32 33 syl2anc φ x I F x dist x I R x G x = x I F x E G x
35 25 34 eqtrid φ y I F y dist x I R y G y = x I F x E G x
36 35 rneqd φ ran y I F y dist x I R y G y = ran x I F x E G x
37 36 uneq1d φ ran y I F y dist x I R y G y 0 = ran x I F x E G x 0
38 37 supeq1d φ sup ran y I F y dist x I R y G y 0 * < = sup ran x I F x E G x 0 * <
39 13 38 eqtrd φ F D G = sup ran x I F x E G x 0 * <