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

Proof

Step Hyp Ref Expression
1 prdsbasmpt.y Y = S 𝑠 R
2 prdsbasmpt.b B = Base Y
3 prdsbasmpt.s φ S V
4 prdsbasmpt.i φ I W
5 prdsbasmpt.r φ R Fn I
6 prdsplusgval.f φ F B
7 prdsplusgval.g φ G B
8 prdsdsval.d D = dist Y
9 fnex R Fn I I W R V
10 5 4 9 syl2anc φ R V
11 fndm R Fn I dom R = I
12 5 11 syl φ dom R = I
13 1 3 10 2 12 8 prdsds φ D = f B , g B sup ran x I f x dist R x g x 0 * <
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 φ f = F g = G f x dist R x g x = F x dist R x G x
18 17 mpteq2dv φ f = F g = G x I f x dist R x g x = x I F x dist R x G x
19 18 rneqd φ f = F g = G ran x I f x dist R x g x = ran x I F x dist R x G x
20 19 uneq1d φ f = F g = G ran x I f x dist R x g x 0 = ran x I F x dist R x G x 0
21 20 supeq1d φ f = F g = G sup ran x I f x dist R x g x 0 * < = sup ran x I F x dist R x G x 0 * <
22 xrltso < Or *
23 22 supex sup ran x I F x dist R x G x 0 * < V
24 23 a1i φ sup ran x I F x dist R x G x 0 * < V
25 13 21 6 7 24 ovmpod φ F D G = sup ran x I F x dist R x G x 0 * <