MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prdsxmetlem Structured version   Visualization version   GIF version

Theorem prdsxmetlem 22905
Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
Hypotheses
Ref Expression
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
Ref Expression
prdsxmetlem (𝜑𝐷 ∈ (∞Met‘𝐵))
Distinct variable groups:   𝑥,𝐼   𝜑,𝑥   𝑥,𝐵   𝑥,𝐷
Allowed substitution hints:   𝑅(𝑥)   𝑆(𝑥)   𝐸(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑋(𝑥)   𝑌(𝑥)   𝑍(𝑥)

Proof of Theorem prdsxmetlem
Dummy variables 𝑓 𝑔 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prdsdsf.b . . . 4 𝐵 = (Base‘𝑌)
21fvexi 6677 . . 3 𝐵 ∈ V
32a1i 11 . 2 (𝜑𝐵 ∈ V)
4 prdsdsf.y . . . 4 𝑌 = (𝑆Xs(𝑥𝐼𝑅))
5 prdsdsf.v . . . 4 𝑉 = (Base‘𝑅)
6 prdsdsf.e . . . 4 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
7 prdsdsf.d . . . 4 𝐷 = (dist‘𝑌)
8 prdsdsf.s . . . 4 (𝜑𝑆𝑊)
9 prdsdsf.i . . . 4 (𝜑𝐼𝑋)
10 prdsdsf.r . . . 4 ((𝜑𝑥𝐼) → 𝑅𝑍)
11 prdsdsf.m . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
124, 1, 5, 6, 7, 8, 9, 10, 11prdsdsf 22904 . . 3 (𝜑𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
13 iccssxr 12807 . . 3 (0[,]+∞) ⊆ ℝ*
14 fss 6520 . . 3 ((𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → 𝐷:(𝐵 × 𝐵)⟶ℝ*)
1512, 13, 14sylancl 586 . 2 (𝜑𝐷:(𝐵 × 𝐵)⟶ℝ*)
1612fovrnda 7308 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]+∞))
17 elxrge0 12833 . . . 4 ((𝑓𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝑓𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐷𝑔)))
1817simprbi 497 . . 3 ((𝑓𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝑓𝐷𝑔))
1916, 18syl 17 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ≤ (𝑓𝐷𝑔))
208adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
219adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼𝑋)
2210ralrimiva 3179 . . . . . 6 (𝜑 → ∀𝑥𝐼 𝑅𝑍)
2322adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 𝑅𝑍)
24 simprl 767 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
25 simprr 769 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
264, 1, 20, 21, 23, 24, 25, 5, 6, 7prdsdsval3 16746 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
2726breq1d 5067 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0))
2811adantlr 711 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
294, 1, 20, 21, 23, 5, 24prdsbascl 16744 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
3029r19.21bi 3205 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
314, 1, 20, 21, 23, 5, 25prdsbascl 16744 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
3231r19.21bi 3205 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
33 xmetcl 22868 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3428, 30, 32, 33syl3anc 1363 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3534fmpttd 6871 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
3635frnd 6514 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
37 0xr 10676 . . . . . . 7 0 ∈ ℝ*
3837a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ*)
3938snssd 4734 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ*)
4036, 39unssd 4159 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
41 supxrleub 12707 . . . 4 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
4240, 37, 41sylancl 586 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
43 0le0 11726 . . . . . . 7 0 ≤ 0
44 c0ex 10623 . . . . . . . 8 0 ∈ V
45 breq1 5060 . . . . . . . 8 (𝑧 = 0 → (𝑧 ≤ 0 ↔ 0 ≤ 0))
4644, 45ralsn 4611 . . . . . . 7 (∀𝑧 ∈ {0}𝑧 ≤ 0 ↔ 0 ≤ 0)
4743, 46mpbir 232 . . . . . 6 𝑧 ∈ {0}𝑧 ≤ 0
48 ralunb 4164 . . . . . 6 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ∧ ∀𝑧 ∈ {0}𝑧 ≤ 0))
4947, 48mpbiran2 706 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0)
50 ovex 7178 . . . . . . 7 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
5150rgenw 3147 . . . . . 6 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
52 eqid 2818 . . . . . . 7 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
53 breq1 5060 . . . . . . 7 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ 0 ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5452, 53ralrnmptw 6852 . . . . . 6 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5551, 54ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
5649, 55bitri 276 . . . 4 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
57 xmetge0 22881 . . . . . . . . 9 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
5828, 30, 32, 57syl3anc 1363 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
5958biantrud 532 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
60 xrletri3 12535 . . . . . . . 8 ((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ 0 ∈ ℝ*) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
6134, 37, 60sylancl 586 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
62 xmeteq0 22875 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6328, 30, 32, 62syl3anc 1363 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6459, 61, 633bitr2d 308 . . . . . 6 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6564ralbidva 3193 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
66 eqid 2818 . . . . . . . . . 10 (𝑥𝐼𝑅) = (𝑥𝐼𝑅)
6766fnmpt 6481 . . . . . . . . 9 (∀𝑥𝐼 𝑅𝑍 → (𝑥𝐼𝑅) Fn 𝐼)
6822, 67syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐼𝑅) Fn 𝐼)
6968adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼𝑅) Fn 𝐼)
704, 1, 20, 21, 69, 24prdsbasfn 16732 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 Fn 𝐼)
714, 1, 20, 21, 69, 25prdsbasfn 16732 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 Fn 𝐼)
72 eqfnfv 6794 . . . . . 6 ((𝑓 Fn 𝐼𝑔 Fn 𝐼) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7370, 71, 72syl2anc 584 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7465, 73bitr4d 283 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ 𝑓 = 𝑔))
7556, 74syl5bb 284 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ 𝑓 = 𝑔))
7627, 42, 753bitrd 306 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ 𝑓 = 𝑔))
77263adantr3 1163 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
78773adant3 1124 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
79113ad2antl1 1177 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
80293adantr3 1163 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
81803adant3 1124 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8281r19.21bi 3205 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
83313adantr3 1163 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
84833adant3 1124 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
8584r19.21bi 3205 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
8679, 82, 85, 33syl3anc 1363 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
8783ad2ant1 1125 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑆𝑊)
8893ad2ant1 1125 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐼𝑋)
89223ad2ant1 1125 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 𝑅𝑍)
90 simp23 1200 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐵)
914, 1, 87, 88, 89, 5, 90prdsbascl 16744 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑥) ∈ 𝑉)
9291r19.21bi 3205 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝑉)
93 xmetcl 22868 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
9479, 92, 82, 93syl3anc 1363 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
95 simp3l 1193 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ ℝ)
9695adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) ∈ ℝ)
97 xmetge0 22881 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
9879, 92, 82, 97syl3anc 1363 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
9994fmpttd 6871 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ*)
10099frnd 6514 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
10137a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ∈ ℝ*)
102101snssd 4734 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → {0} ⊆ ℝ*)
103100, 102unssd 4159 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
104 ssun1 4145 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})
105 ovex 7178 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑓𝑥)) ∈ V
106105elabrex 6993 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
107106adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
108 eqid 2818 . . . . . . . . . . . . . . . 16 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥)))
109108rnmpt 5820 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))}
110107, 109eleqtrrdi 2921 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))))
111104, 110sseldi 3962 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}))
112 supxrub 12705 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
113103, 111, 112syl2an2r 681 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
114 simp21 1198 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑓𝐵)
1154, 1, 87, 88, 89, 90, 114, 5, 6, 7prdsdsval3 16746 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
116115adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
117113, 116breqtrrd 5085 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))
118 xrrege0 12555 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ* ∧ (𝐷𝑓) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑓𝑥)) ∧ ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
11994, 96, 98, 117, 118syl22anc 834 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
120 xmetcl 22868 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
12179, 92, 85, 120syl3anc 1363 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
122 simp3r 1194 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ ℝ)
123122adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) ∈ ℝ)
124 xmetge0 22881 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
12579, 92, 85, 124syl3anc 1363 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
126121fmpttd 6871 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
127126frnd 6514 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
128127, 102unssd 4159 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
129 ssun1 4145 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})
130 ovex 7178 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑔𝑥)) ∈ V
131130elabrex 6993 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
132131adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
133 eqid 2818 . . . . . . . . . . . . . . . 16 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥)))
134133rnmpt 5820 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))}
135132, 134eleqtrrdi 2921 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))))
136129, 135sseldi 3962 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}))
137 supxrub 12705 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
138128, 136, 137syl2an2r 681 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
139 simp22 1199 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑔𝐵)
1404, 1, 87, 88, 89, 90, 139, 5, 6, 7prdsdsval3 16746 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
141140adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
142138, 141breqtrrd 5085 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))
143 xrrege0 12555 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (𝐷𝑔) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑔𝑥)) ∧ ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
144121, 123, 125, 142, 143syl22anc 834 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
145119, 144readdcld 10658 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ)
14679, 82, 85, 57syl3anc 1363 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
147 xmettri2 22877 . . . . . . . . . . 11 ((𝐸 ∈ (∞Met‘𝑉) ∧ ((𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
14879, 92, 82, 85, 147syl13anc 1364 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
149119, 144rexaddd 12615 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
150148, 149breqtrd 5083 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
151 xrrege0 12555 . . . . . . . . 9 (((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ) ∧ (0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
15286, 145, 146, 150, 151syl22anc 834 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
153 readdcl 10608 . . . . . . . . . 10 (((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
1541533ad2ant3 1127 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
155154adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
156119, 144, 96, 123, 117, 142le2addd 11247 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ≤ ((𝐷𝑓) + (𝐷𝑔)))
157152, 145, 155, 150, 156letrd 10785 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
158157ralrimiva 3179 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
15986ralrimiva 3179 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
160 breq1 5060 . . . . . . . 8 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
16152, 160ralrnmptw 6852 . . . . . . 7 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
162159, 161syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
163158, 162mpbird 258 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
164123ad2ant1 1125 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
165164, 90, 114fovrnd 7309 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ (0[,]+∞))
166 elxrge0 12833 . . . . . . . . 9 ((𝐷𝑓) ∈ (0[,]+∞) ↔ ((𝐷𝑓) ∈ ℝ* ∧ 0 ≤ (𝐷𝑓)))
167166simprbi 497 . . . . . . . 8 ((𝐷𝑓) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑓))
168165, 167syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑓))
169164, 90, 139fovrnd 7309 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ (0[,]+∞))
170 elxrge0 12833 . . . . . . . . 9 ((𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝐷𝑔)))
171170simprbi 497 . . . . . . . 8 ((𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑔))
172169, 171syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑔))
17395, 122, 168, 172addge0d 11204 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
174 breq1 5060 . . . . . . 7 (𝑧 = 0 → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔))))
17544, 174ralsn 4611 . . . . . 6 (∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
176173, 175sylibr 235 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
177 ralunb 4164 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ∧ ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
178163, 176, 177sylanbrc 583 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
179403adantr3 1163 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
1801793adant3 1124 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
181154rexrd 10679 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*)
182 supxrleub 12707 . . . . 5 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
183180, 181, 182syl2anc 584 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
184178, 183mpbird 258 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)))
18578, 184eqbrtrd 5079 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) ≤ ((𝐷𝑓) + (𝐷𝑔)))
1863, 15, 19, 76, 185isxmet2d 22864 1 (𝜑𝐷 ∈ (∞Met‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wcel 2105  {cab 2796  wral 3135  wrex 3136  Vcvv 3492  cun 3931  wss 3933  {csn 4557   class class class wbr 5057  cmpt 5137   × cxp 5546  ran crn 5549  cres 5550   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  supcsup 8892  cr 10524  0cc0 10525   + caddc 10528  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664   +𝑒 cxad 12493  [,]cicc 12729  Basecbs 16471  distcds 16562  Xscprds 16707  ∞Metcxmet 20458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-map 8397  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-sup 8894  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-icc 12733  df-fz 12881  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-plusg 16566  df-mulr 16567  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-hom 16577  df-cco 16578  df-prds 16709  df-xmet 20466
This theorem is referenced by:  prdsxmet  22906
  Copyright terms: Public domain W3C validator