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

Theorem prdsxmetlem 22086
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‘𝑌)
2 fvex 6160 . . . 4 (Base‘𝑌) ∈ V
31, 2eqeltri 2694 . . 3 𝐵 ∈ V
43a1i 11 . 2 (𝜑𝐵 ∈ V)
5 prdsdsf.y . . . 4 𝑌 = (𝑆Xs(𝑥𝐼𝑅))
6 prdsdsf.v . . . 4 𝑉 = (Base‘𝑅)
7 prdsdsf.e . . . 4 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
8 prdsdsf.d . . . 4 𝐷 = (dist‘𝑌)
9 prdsdsf.s . . . 4 (𝜑𝑆𝑊)
10 prdsdsf.i . . . 4 (𝜑𝐼𝑋)
11 prdsdsf.r . . . 4 ((𝜑𝑥𝐼) → 𝑅𝑍)
12 prdsdsf.m . . . 4 ((𝜑𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
135, 1, 6, 7, 8, 9, 10, 11, 12prdsdsf 22085 . . 3 (𝜑𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
14 iccssxr 12201 . . 3 (0[,]+∞) ⊆ ℝ*
15 fss 6015 . . 3 ((𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → 𝐷:(𝐵 × 𝐵)⟶ℝ*)
1613, 14, 15sylancl 693 . 2 (𝜑𝐷:(𝐵 × 𝐵)⟶ℝ*)
1713fovrnda 6761 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]+∞))
18 elxrge0 12226 . . . 4 ((𝑓𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝑓𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐷𝑔)))
1918simprbi 480 . . 3 ((𝑓𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝑓𝐷𝑔))
2017, 19syl 17 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ≤ (𝑓𝐷𝑔))
219adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
2210adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼𝑋)
2311ralrimiva 2960 . . . . . 6 (𝜑 → ∀𝑥𝐼 𝑅𝑍)
2423adantr 481 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 𝑅𝑍)
25 simprl 793 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
26 simprr 795 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
275, 1, 21, 22, 24, 25, 26, 6, 7, 8prdsdsval3 16069 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
2827breq1d 4625 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0))
2912adantlr 750 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
305, 1, 21, 22, 24, 6, 25prdsbascl 16067 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
3130r19.21bi 2927 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
325, 1, 21, 22, 24, 6, 26prdsbascl 16067 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
3332r19.21bi 2927 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
34 xmetcl 22049 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3529, 31, 33, 34syl3anc 1323 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
36 eqid 2621 . . . . . . 7 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
3735, 36fmptd 6343 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
38 frn 6012 . . . . . 6 ((𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
3937, 38syl 17 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
40 0xr 10033 . . . . . . 7 0 ∈ ℝ*
4140a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ*)
4241snssd 4311 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ*)
4339, 42unssd 3769 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
44 supxrleub 12102 . . . 4 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
4543, 40, 44sylancl 693 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
46 0le0 11057 . . . . . . 7 0 ≤ 0
47 c0ex 9981 . . . . . . . 8 0 ∈ V
48 breq1 4618 . . . . . . . 8 (𝑧 = 0 → (𝑧 ≤ 0 ↔ 0 ≤ 0))
4947, 48ralsn 4195 . . . . . . 7 (∀𝑧 ∈ {0}𝑧 ≤ 0 ↔ 0 ≤ 0)
5046, 49mpbir 221 . . . . . 6 𝑧 ∈ {0}𝑧 ≤ 0
51 ralunb 3774 . . . . . 6 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ∧ ∀𝑧 ∈ {0}𝑧 ≤ 0))
5250, 51mpbiran2 953 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0)
53 ovex 6635 . . . . . . 7 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
5453rgenw 2919 . . . . . 6 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
55 breq1 4618 . . . . . . 7 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ 0 ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5636, 55ralrnmpt 6326 . . . . . 6 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5754, 56ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
5852, 57bitri 264 . . . 4 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
59 xmetge0 22062 . . . . . . . . 9 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6029, 31, 33, 59syl3anc 1323 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6160biantrud 528 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
62 xrletri3 11932 . . . . . . . 8 ((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ 0 ∈ ℝ*) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
6335, 40, 62sylancl 693 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
64 xmeteq0 22056 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6529, 31, 33, 64syl3anc 1323 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6661, 63, 653bitr2d 296 . . . . . 6 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6766ralbidva 2979 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
68 eqid 2621 . . . . . . . . . 10 (𝑥𝐼𝑅) = (𝑥𝐼𝑅)
6968fnmpt 5979 . . . . . . . . 9 (∀𝑥𝐼 𝑅𝑍 → (𝑥𝐼𝑅) Fn 𝐼)
7023, 69syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐼𝑅) Fn 𝐼)
7170adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼𝑅) Fn 𝐼)
725, 1, 21, 22, 71, 25prdsbasfn 16055 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 Fn 𝐼)
735, 1, 21, 22, 71, 26prdsbasfn 16055 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 Fn 𝐼)
74 eqfnfv 6269 . . . . . 6 ((𝑓 Fn 𝐼𝑔 Fn 𝐼) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7572, 73, 74syl2anc 692 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7667, 75bitr4d 271 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ 𝑓 = 𝑔))
7758, 76syl5bb 272 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ 𝑓 = 𝑔))
7828, 45, 773bitrd 294 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ 𝑓 = 𝑔))
79273adantr3 1220 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
80793adant3 1079 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
81123ad2antl1 1221 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
82303adantr3 1220 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
83823adant3 1079 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8483r19.21bi 2927 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
85323adantr3 1220 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
86853adant3 1079 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
8786r19.21bi 2927 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
8881, 84, 87, 34syl3anc 1323 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
8993ad2ant1 1080 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑆𝑊)
90103ad2ant1 1080 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐼𝑋)
91233ad2ant1 1080 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 𝑅𝑍)
92 simp23 1094 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐵)
935, 1, 89, 90, 91, 6, 92prdsbascl 16067 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑥) ∈ 𝑉)
9493r19.21bi 2927 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝑉)
95 xmetcl 22049 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
9681, 94, 84, 95syl3anc 1323 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
97 simp3l 1087 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ ℝ)
9897adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) ∈ ℝ)
99 xmetge0 22062 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
10081, 94, 84, 99syl3anc 1323 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
101 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥)))
10296, 101fmptd 6343 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ*)
103 frn 6012 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
10540a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ∈ ℝ*)
106105snssd 4311 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → {0} ⊆ ℝ*)
107104, 106unssd 3769 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
108107adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
109 ssun1 3756 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})
110 ovex 6635 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑓𝑥)) ∈ V
111110elabrex 6458 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
112111adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
113101rnmpt 5333 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))}
114112, 113syl6eleqr 2709 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))))
115109, 114sseldi 3582 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}))
116 supxrub 12100 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
117108, 115, 116syl2anc 692 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
118 simp21 1092 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑓𝐵)
1195, 1, 89, 90, 91, 92, 118, 6, 7, 8prdsdsval3 16069 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
120119adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
121117, 120breqtrrd 4643 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))
122 xrrege0 11951 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ* ∧ (𝐷𝑓) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑓𝑥)) ∧ ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
12396, 98, 100, 121, 122syl22anc 1324 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
124 xmetcl 22049 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
12581, 94, 87, 124syl3anc 1323 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
126 simp3r 1088 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ ℝ)
127126adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) ∈ ℝ)
128 xmetge0 22062 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
12981, 94, 87, 128syl3anc 1323 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
130 eqid 2621 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥)))
131125, 130fmptd 6343 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
132 frn 6012 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
133131, 132syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
134133, 106unssd 3769 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
135134adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
136 ssun1 3756 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})
137 ovex 6635 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑔𝑥)) ∈ V
138137elabrex 6458 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
139138adantl 482 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
140130rnmpt 5333 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))}
141139, 140syl6eleqr 2709 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))))
142136, 141sseldi 3582 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}))
143 supxrub 12100 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
144135, 142, 143syl2anc 692 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
145 simp22 1093 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑔𝐵)
1465, 1, 89, 90, 91, 92, 145, 6, 7, 8prdsdsval3 16069 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
147146adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
148144, 147breqtrrd 4643 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))
149 xrrege0 11951 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (𝐷𝑔) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑔𝑥)) ∧ ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
150125, 127, 129, 148, 149syl22anc 1324 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
151123, 150readdcld 10016 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ)
15281, 84, 87, 59syl3anc 1323 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
153 xmettri2 22058 . . . . . . . . . . 11 ((𝐸 ∈ (∞Met‘𝑉) ∧ ((𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
15481, 94, 84, 87, 153syl13anc 1325 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
155 rexadd 12009 . . . . . . . . . . 11 ((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
156123, 150, 155syl2anc 692 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
157154, 156breqtrd 4641 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
158 xrrege0 11951 . . . . . . . . 9 (((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ) ∧ (0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
15988, 151, 152, 157, 158syl22anc 1324 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
160 readdcl 9966 . . . . . . . . . 10 (((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
1611603ad2ant3 1082 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
162161adantr 481 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
163123, 150, 98, 127, 121, 148le2addd 10593 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ≤ ((𝐷𝑓) + (𝐷𝑔)))
164159, 151, 162, 157, 163letrd 10141 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
165164ralrimiva 2960 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
16688ralrimiva 2960 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
167 breq1 4618 . . . . . . . 8 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
16836, 167ralrnmpt 6326 . . . . . . 7 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
169166, 168syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
170165, 169mpbird 247 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
171133ad2ant1 1080 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
172171, 92, 118fovrnd 6762 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ (0[,]+∞))
173 elxrge0 12226 . . . . . . . . 9 ((𝐷𝑓) ∈ (0[,]+∞) ↔ ((𝐷𝑓) ∈ ℝ* ∧ 0 ≤ (𝐷𝑓)))
174173simprbi 480 . . . . . . . 8 ((𝐷𝑓) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑓))
175172, 174syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑓))
176171, 92, 145fovrnd 6762 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ (0[,]+∞))
177 elxrge0 12226 . . . . . . . . 9 ((𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝐷𝑔)))
178177simprbi 480 . . . . . . . 8 ((𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑔))
179176, 178syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑔))
18097, 126, 175, 179addge0d 10550 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
181 breq1 4618 . . . . . . 7 (𝑧 = 0 → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔))))
18247, 181ralsn 4195 . . . . . 6 (∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
183180, 182sylibr 224 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
184 ralunb 3774 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ∧ ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
185170, 183, 184sylanbrc 697 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
186433adantr3 1220 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
1871863adant3 1079 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
188161rexrd 10036 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*)
189 supxrleub 12102 . . . . 5 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
190187, 188, 189syl2anc 692 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
191185, 190mpbird 247 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)))
19280, 191eqbrtrd 4637 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) ≤ ((𝐷𝑓) + (𝐷𝑔)))
1934, 16, 20, 78, 192isxmet2d 22045 1 (𝜑𝐷 ∈ (∞Met‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  {cab 2607  wral 2907  wrex 2908  Vcvv 3186  cun 3554  wss 3556  {csn 4150   class class class wbr 4615  cmpt 4675   × cxp 5074  ran crn 5077  cres 5078   Fn wfn 5844  wf 5845  cfv 5849  (class class class)co 6607  supcsup 8293  cr 9882  0cc0 9883   + caddc 9886  +∞cpnf 10018  *cxr 10020   < clt 10021  cle 10022   +𝑒 cxad 11891  [,]cicc 12123  Basecbs 15784  distcds 15874  Xscprds 16030  ∞Metcxmt 19653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-sup 8295  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-uz 11635  df-rp 11780  df-xneg 11893  df-xadd 11894  df-xmul 11895  df-icc 12127  df-fz 12272  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-plusg 15878  df-mulr 15879  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-hom 15890  df-cco 15891  df-prds 16032  df-xmet 19661
This theorem is referenced by:  prdsxmet  22087
  Copyright terms: Public domain W3C validator