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

Theorem prdsxmetlem 22452
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 6389 . . 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 22451 . . 3 (𝜑𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
13 iccssxr 12458 . . 3 (0[,]+∞) ⊆ ℝ*
14 fss 6236 . . 3 ((𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → 𝐷:(𝐵 × 𝐵)⟶ℝ*)
1512, 13, 14sylancl 580 . 2 (𝜑𝐷:(𝐵 × 𝐵)⟶ℝ*)
1612fovrnda 7003 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]+∞))
17 elxrge0 12485 . . . 4 ((𝑓𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝑓𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐷𝑔)))
1817simprbi 490 . . 3 ((𝑓𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝑓𝐷𝑔))
1916, 18syl 17 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ≤ (𝑓𝐷𝑔))
208adantr 472 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
219adantr 472 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼𝑋)
2210ralrimiva 3113 . . . . . 6 (𝜑 → ∀𝑥𝐼 𝑅𝑍)
2322adantr 472 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 𝑅𝑍)
24 simprl 787 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
25 simprr 789 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
264, 1, 20, 21, 23, 24, 25, 5, 6, 7prdsdsval3 16413 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
2726breq1d 4819 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0))
2811adantlr 706 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
294, 1, 20, 21, 23, 5, 24prdsbascl 16411 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
3029r19.21bi 3079 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
314, 1, 20, 21, 23, 5, 25prdsbascl 16411 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
3231r19.21bi 3079 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
33 xmetcl 22415 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3428, 30, 32, 33syl3anc 1490 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3534fmpttd 6575 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
3635frnd 6230 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
37 0xr 10340 . . . . . . 7 0 ∈ ℝ*
3837a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ*)
3938snssd 4494 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ*)
4036, 39unssd 3951 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
41 supxrleub 12358 . . . 4 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
4240, 37, 41sylancl 580 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
43 0le0 11380 . . . . . . 7 0 ≤ 0
44 c0ex 10287 . . . . . . . 8 0 ∈ V
45 breq1 4812 . . . . . . . 8 (𝑧 = 0 → (𝑧 ≤ 0 ↔ 0 ≤ 0))
4644, 45ralsn 4379 . . . . . . 7 (∀𝑧 ∈ {0}𝑧 ≤ 0 ↔ 0 ≤ 0)
4743, 46mpbir 222 . . . . . 6 𝑧 ∈ {0}𝑧 ≤ 0
48 ralunb 3956 . . . . . 6 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ∧ ∀𝑧 ∈ {0}𝑧 ≤ 0))
4947, 48mpbiran2 701 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0)
50 ovex 6874 . . . . . . 7 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
5150rgenw 3071 . . . . . 6 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
52 eqid 2765 . . . . . . 7 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
53 breq1 4812 . . . . . . 7 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ 0 ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5452, 53ralrnmpt 6558 . . . . . 6 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5551, 54ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
5649, 55bitri 266 . . . 4 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
57 xmetge0 22428 . . . . . . . . 9 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
5828, 30, 32, 57syl3anc 1490 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
5958biantrud 527 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
60 xrletri3 12187 . . . . . . . 8 ((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ 0 ∈ ℝ*) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
6134, 37, 60sylancl 580 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
62 xmeteq0 22422 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6328, 30, 32, 62syl3anc 1490 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6459, 61, 633bitr2d 298 . . . . . 6 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6564ralbidva 3132 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
66 eqid 2765 . . . . . . . . . 10 (𝑥𝐼𝑅) = (𝑥𝐼𝑅)
6766fnmpt 6198 . . . . . . . . 9 (∀𝑥𝐼 𝑅𝑍 → (𝑥𝐼𝑅) Fn 𝐼)
6822, 67syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐼𝑅) Fn 𝐼)
6968adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼𝑅) Fn 𝐼)
704, 1, 20, 21, 69, 24prdsbasfn 16399 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 Fn 𝐼)
714, 1, 20, 21, 69, 25prdsbasfn 16399 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 Fn 𝐼)
72 eqfnfv 6501 . . . . . 6 ((𝑓 Fn 𝐼𝑔 Fn 𝐼) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7370, 71, 72syl2anc 579 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7465, 73bitr4d 273 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ 𝑓 = 𝑔))
7556, 74syl5bb 274 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ 𝑓 = 𝑔))
7627, 42, 753bitrd 296 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ 𝑓 = 𝑔))
77263adantr3 1212 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
78773adant3 1162 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
79113ad2antl1 1236 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
80293adantr3 1212 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
81803adant3 1162 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8281r19.21bi 3079 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
83313adantr3 1212 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
84833adant3 1162 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
8584r19.21bi 3079 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
8679, 82, 85, 33syl3anc 1490 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
8783ad2ant1 1163 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑆𝑊)
8893ad2ant1 1163 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐼𝑋)
89223ad2ant1 1163 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 𝑅𝑍)
90 simp23 1265 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐵)
914, 1, 87, 88, 89, 5, 90prdsbascl 16411 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑥) ∈ 𝑉)
9291r19.21bi 3079 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝑉)
93 xmetcl 22415 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
9479, 92, 82, 93syl3anc 1490 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
95 simp3l 1258 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ ℝ)
9695adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) ∈ ℝ)
97 xmetge0 22428 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
9879, 92, 82, 97syl3anc 1490 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
9994fmpttd 6575 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ*)
10099frnd 6230 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
10137a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ∈ ℝ*)
102101snssd 4494 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → {0} ⊆ ℝ*)
103100, 102unssd 3951 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
104103adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
105 ssun1 3938 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})
106 ovex 6874 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑓𝑥)) ∈ V
107106elabrex 6693 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
108107adantl 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
109 eqid 2765 . . . . . . . . . . . . . . . 16 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥)))
110109rnmpt 5540 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))}
111108, 110syl6eleqr 2855 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))))
112105, 111sseldi 3759 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}))
113 supxrub 12356 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
114104, 112, 113syl2anc 579 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
115 simp21 1263 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑓𝐵)
1164, 1, 87, 88, 89, 90, 115, 5, 6, 7prdsdsval3 16413 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
117116adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
118114, 117breqtrrd 4837 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))
119 xrrege0 12207 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ* ∧ (𝐷𝑓) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑓𝑥)) ∧ ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
12094, 96, 98, 118, 119syl22anc 867 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
121 xmetcl 22415 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
12279, 92, 85, 121syl3anc 1490 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
123 simp3r 1259 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ ℝ)
124123adantr 472 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) ∈ ℝ)
125 xmetge0 22428 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
12679, 92, 85, 125syl3anc 1490 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
127122fmpttd 6575 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
128127frnd 6230 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
129128, 102unssd 3951 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
130129adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
131 ssun1 3938 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})
132 ovex 6874 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑔𝑥)) ∈ V
133132elabrex 6693 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
134133adantl 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
135 eqid 2765 . . . . . . . . . . . . . . . 16 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥)))
136135rnmpt 5540 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))}
137134, 136syl6eleqr 2855 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))))
138131, 137sseldi 3759 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}))
139 supxrub 12356 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
140130, 138, 139syl2anc 579 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
141 simp22 1264 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑔𝐵)
1424, 1, 87, 88, 89, 90, 141, 5, 6, 7prdsdsval3 16413 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
143142adantr 472 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
144140, 143breqtrrd 4837 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))
145 xrrege0 12207 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (𝐷𝑔) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑔𝑥)) ∧ ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
146122, 124, 126, 144, 145syl22anc 867 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
147120, 146readdcld 10323 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ)
14879, 82, 85, 57syl3anc 1490 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
149 xmettri2 22424 . . . . . . . . . . 11 ((𝐸 ∈ (∞Met‘𝑉) ∧ ((𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
15079, 92, 82, 85, 149syl13anc 1491 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
151 rexadd 12265 . . . . . . . . . . 11 ((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
152120, 146, 151syl2anc 579 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
153150, 152breqtrd 4835 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
154 xrrege0 12207 . . . . . . . . 9 (((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ) ∧ (0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
15586, 147, 148, 153, 154syl22anc 867 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
156 readdcl 10272 . . . . . . . . . 10 (((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
1571563ad2ant3 1165 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
158157adantr 472 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
159120, 146, 96, 124, 118, 144le2addd 10900 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ≤ ((𝐷𝑓) + (𝐷𝑔)))
160155, 147, 158, 153, 159letrd 10448 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
161160ralrimiva 3113 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
16286ralrimiva 3113 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
163 breq1 4812 . . . . . . . 8 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
16452, 163ralrnmpt 6558 . . . . . . 7 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
165162, 164syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
166161, 165mpbird 248 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
167123ad2ant1 1163 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
168167, 90, 115fovrnd 7004 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ (0[,]+∞))
169 elxrge0 12485 . . . . . . . . 9 ((𝐷𝑓) ∈ (0[,]+∞) ↔ ((𝐷𝑓) ∈ ℝ* ∧ 0 ≤ (𝐷𝑓)))
170169simprbi 490 . . . . . . . 8 ((𝐷𝑓) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑓))
171168, 170syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑓))
172167, 90, 141fovrnd 7004 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ (0[,]+∞))
173 elxrge0 12485 . . . . . . . . 9 ((𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝐷𝑔)))
174173simprbi 490 . . . . . . . 8 ((𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑔))
175172, 174syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑔))
17695, 123, 171, 175addge0d 10857 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
177 breq1 4812 . . . . . . 7 (𝑧 = 0 → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔))))
17844, 177ralsn 4379 . . . . . 6 (∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
179176, 178sylibr 225 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
180 ralunb 3956 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ∧ ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
181166, 179, 180sylanbrc 578 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
182403adantr3 1212 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
1831823adant3 1162 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
184157rexrd 10343 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*)
185 supxrleub 12358 . . . . 5 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
186183, 184, 185syl2anc 579 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
187181, 186mpbird 248 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)))
18878, 187eqbrtrd 4831 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) ≤ ((𝐷𝑓) + (𝐷𝑔)))
1893, 15, 19, 76, 188isxmet2d 22411 1 (𝜑𝐷 ∈ (∞Met‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  {cab 2751  wral 3055  wrex 3056  Vcvv 3350  cun 3730  wss 3732  {csn 4334   class class class wbr 4809  cmpt 4888   × cxp 5275  ran crn 5278  cres 5279   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  supcsup 8553  cr 10188  0cc0 10189   + caddc 10192  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329   +𝑒 cxad 12144  [,]cicc 12380  Basecbs 16132  distcds 16225  Xscprds 16374  ∞Metcxmet 20004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-map 8062  df-ixp 8114  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-icc 12384  df-fz 12534  df-struct 16134  df-ndx 16135  df-slot 16136  df-base 16138  df-plusg 16229  df-mulr 16230  df-sca 16232  df-vsca 16233  df-ip 16234  df-tset 16235  df-ple 16236  df-ds 16238  df-hom 16240  df-cco 16241  df-prds 16376  df-xmet 20012
This theorem is referenced by:  prdsxmet  22453
  Copyright terms: Public domain W3C validator