Metamath Proof Explorer

Theorem prdsdsf

Description: The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
Assertion prdsdsf ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2 prdsdsf.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsdsf.v ⊢ 𝑉 = ( Base ‘ 𝑅 )
4 prdsdsf.e ⊢ 𝐸 = ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) )
5 prdsdsf.d ⊢ 𝐷 = ( dist ‘ 𝑌 )
6 prdsdsf.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑊 )
7 prdsdsf.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑋 )
8 prdsdsf.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ 𝑍 )
9 prdsdsf.m ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
10 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
11 8 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 ∈ V )
12 11 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ V )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ V )
14 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑅
15 14 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V
16 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑅 = ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
17 16 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝑅 ∈ V ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V ) )
18 15 17 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V ) )
19 13 18 mpan9 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V )
20 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
21 20 fvmpts ⊢ ( ( 𝑦 ∈ 𝐼 ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ∈ V ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
22 10 19 21 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
23 22 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) = ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
24 23 oveqd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ( 𝑔 ‘ 𝑦 ) ) )
25 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑆 ∈ 𝑊 )
26 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑋 )
27 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑓 ∈ 𝐵 )
28 1 2 25 26 13 3 27 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 )
29 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝑉
30 29 nfel2 ⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉
31 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) )
32 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝑉 = ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
33 31 32 eleq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 ↔ ( 𝑓 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
34 30 33 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 ( 𝑓 ‘ 𝑥 ) ∈ 𝑉 → ( 𝑓 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
35 28 34 mpan9 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
36 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 𝑔 ∈ 𝐵 )
37 1 2 25 26 13 3 36 prdsbascl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 )
38 29 nfel2 ⊢ Ⅎ 𝑥 ( 𝑔 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉
39 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) )
40 39 32 eleq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 ↔ ( 𝑔 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
41 38 40 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 ( 𝑔 ‘ 𝑥 ) ∈ 𝑉 → ( 𝑔 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
42 37 41 mpan9 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
43 35 42 ovresd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑦 ) ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ( 𝑔 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ( 𝑔 ‘ 𝑦 ) ) )
44 24 43 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) = ( ( 𝑓 ‘ 𝑦 ) ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ( 𝑔 ‘ 𝑦 ) ) )
45 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 𝐸 ∈ ( ∞Met ‘ 𝑉 ) )
47 nfcv ⊢ Ⅎ 𝑥 dist
48 47 14 nffv ⊢ Ⅎ 𝑥 ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 )
49 29 29 nfxp ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
50 48 49 nfres ⊢ Ⅎ 𝑥 ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
51 nfcv ⊢ Ⅎ 𝑥 ∞Met
52 51 29 nffv ⊢ Ⅎ 𝑥 ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
53 50 52 nfel ⊢ Ⅎ 𝑥 ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ∈ ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 )
54 16 fveq2d ⊢ ( 𝑥 = 𝑦 → ( dist ‘ 𝑅 ) = ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) )
55 32 sqxpeqd ⊢ ( 𝑥 = 𝑦 → ( 𝑉 × 𝑉 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
56 54 55 reseq12d ⊢ ( 𝑥 = 𝑦 → ( ( dist ‘ 𝑅 ) ↾ ( 𝑉 × 𝑉 ) ) = ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) )
57 4 56 syl5eq ⊢ ( 𝑥 = 𝑦 → 𝐸 = ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) )
58 32 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ∞Met ‘ 𝑉 ) = ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
59 57 58 eleq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐸 ∈ ( ∞Met ‘ 𝑉 ) ↔ ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ∈ ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) )
60 53 59 rspc ⊢ ( 𝑦 ∈ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 𝐸 ∈ ( ∞Met ‘ 𝑉 ) → ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ∈ ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) )
61 46 60 mpan9 ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ∈ ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) )
62 xmetcl ⊢ ( ( ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ∈ ( ∞Met ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ∧ ( 𝑓 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ∧ ( 𝑔 ‘ 𝑦 ) ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) → ( ( 𝑓 ‘ 𝑦 ) ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ( 𝑔 ‘ 𝑦 ) ) ∈ ℝ* )
63 61 35 42 62 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑦 ) ( ( dist ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝑅 ) ↾ ( ⦋ 𝑦 / 𝑥 ⦌ 𝑉 × ⦋ 𝑦 / 𝑥 ⦌ 𝑉 ) ) ( 𝑔 ‘ 𝑦 ) ) ∈ ℝ* )
64 44 63 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ∈ ℝ* )
65 64 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) : 𝐼 ⟶ ℝ* )
66 65 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ⊆ ℝ* )
67 0xr ⊢ 0 ∈ ℝ*
68 67 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 0 ∈ ℝ* )
69 68 snssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → { 0 } ⊆ ℝ* )
70 66 69 unssd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) ⊆ ℝ* )
71 supxrcl ⊢ ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) ⊆ ℝ* → sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ℝ* )
72 70 71 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ℝ* )
73 ssun2 ⊢ { 0 } ⊆ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } )
74 c0ex ⊢ 0 ∈ V
75 74 snss ⊢ ( 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) ↔ { 0 } ⊆ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) )
76 73 75 mpbir ⊢ 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } )
77 supxrub ⊢ ( ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) ⊆ ℝ* ∧ 0 ∈ ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) ) → 0 ≤ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
78 70 76 77 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → 0 ≤ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
79 elxrge0 ⊢ ( sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ℝ* ∧ 0 ≤ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
80 72 78 79 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) ) → sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
81 80 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
82 eqid ⊢ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) )
83 82 fmpo ⊢ ( ∀ 𝑓 ∈ 𝐵 ∀ 𝑔 ∈ 𝐵 sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )
84 81 83 sylib ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )
85 7 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ∈ V )
86 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 )
87 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑍 → dom ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
88 86 87 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = 𝐼 )
89 1 6 85 2 88 5 prdsds ⊢ ( 𝜑 → 𝐷 = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) )
90 89 feq1d ⊢ ( 𝜑 → ( 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ sup ( ( ran ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ 𝑦 ) ( dist ‘ ( ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) ‘ 𝑦 ) ) ( 𝑔 ‘ 𝑦 ) ) ) ∪ { 0 } ) , ℝ* , < ) ) : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) ) )
91 84 90 mpbird ⊢ ( 𝜑 → 𝐷 : ( 𝐵 × 𝐵 ) ⟶ ( 0 [,] +∞ ) )