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

Theorem prdsxmetlem 22220
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 6239 . . . 4 (Base‘𝑌) ∈ V
31, 2eqeltri 2726 . . 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 22219 . . 3 (𝜑𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
14 iccssxr 12294 . . 3 (0[,]+∞) ⊆ ℝ*
15 fss 6094 . . 3 ((𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → 𝐷:(𝐵 × 𝐵)⟶ℝ*)
1613, 14, 15sylancl 695 . 2 (𝜑𝐷:(𝐵 × 𝐵)⟶ℝ*)
1713fovrnda 6847 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]+∞))
18 elxrge0 12319 . . . 4 ((𝑓𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝑓𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐷𝑔)))
1918simprbi 479 . . 3 ((𝑓𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝑓𝐷𝑔))
2017, 19syl 17 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ≤ (𝑓𝐷𝑔))
219adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
2210adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼𝑋)
2311ralrimiva 2995 . . . . . 6 (𝜑 → ∀𝑥𝐼 𝑅𝑍)
2423adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 𝑅𝑍)
25 simprl 809 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
26 simprr 811 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
275, 1, 21, 22, 24, 25, 26, 6, 7, 8prdsdsval3 16192 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
2827breq1d 4695 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0))
2912adantlr 751 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
305, 1, 21, 22, 24, 6, 25prdsbascl 16190 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
3130r19.21bi 2961 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
325, 1, 21, 22, 24, 6, 26prdsbascl 16190 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
3332r19.21bi 2961 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
34 xmetcl 22183 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3529, 31, 33, 34syl3anc 1366 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
36 eqid 2651 . . . . . . 7 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
3735, 36fmptd 6425 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
38 frn 6091 . . . . . 6 ((𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
3937, 38syl 17 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
40 0xr 10124 . . . . . . 7 0 ∈ ℝ*
4140a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ*)
4241snssd 4372 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ*)
4339, 42unssd 3822 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
44 supxrleub 12194 . . . 4 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ 0 ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
4543, 40, 44sylancl 695 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0 ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0))
46 0le0 11148 . . . . . . 7 0 ≤ 0
47 c0ex 10072 . . . . . . . 8 0 ∈ V
48 breq1 4688 . . . . . . . 8 (𝑧 = 0 → (𝑧 ≤ 0 ↔ 0 ≤ 0))
4947, 48ralsn 4254 . . . . . . 7 (∀𝑧 ∈ {0}𝑧 ≤ 0 ↔ 0 ≤ 0)
5046, 49mpbir 221 . . . . . 6 𝑧 ∈ {0}𝑧 ≤ 0
51 ralunb 3827 . . . . . 6 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ∧ ∀𝑧 ∈ {0}𝑧 ≤ 0))
5250, 51mpbiran2 974 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0)
53 ovex 6718 . . . . . . 7 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
5453rgenw 2953 . . . . . 6 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
55 breq1 4688 . . . . . . 7 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ 0 ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5636, 55ralrnmpt 6408 . . . . . 6 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5754, 56ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
5852, 57bitri 264 . . . 4 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
59 xmetge0 22196 . . . . . . . . 9 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6029, 31, 33, 59syl3anc 1366 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6160biantrud 527 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
62 xrletri3 12023 . . . . . . . 8 ((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ 0 ∈ ℝ*) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
6335, 40, 62sylancl 695 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
64 xmeteq0 22190 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6529, 31, 33, 64syl3anc 1366 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6661, 63, 653bitr2d 296 . . . . . 6 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6766ralbidva 3014 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
68 eqid 2651 . . . . . . . . . 10 (𝑥𝐼𝑅) = (𝑥𝐼𝑅)
6968fnmpt 6058 . . . . . . . . 9 (∀𝑥𝐼 𝑅𝑍 → (𝑥𝐼𝑅) Fn 𝐼)
7023, 69syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐼𝑅) Fn 𝐼)
7170adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼𝑅) Fn 𝐼)
725, 1, 21, 22, 71, 25prdsbasfn 16178 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 Fn 𝐼)
735, 1, 21, 22, 71, 26prdsbasfn 16178 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 Fn 𝐼)
74 eqfnfv 6351 . . . . . 6 ((𝑓 Fn 𝐼𝑔 Fn 𝐼) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7572, 73, 74syl2anc 694 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7667, 75bitr4d 271 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ 𝑓 = 𝑔))
7758, 76syl5bb 272 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ 𝑓 = 𝑔))
7828, 45, 773bitrd 294 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ 𝑓 = 𝑔))
79273adantr3 1242 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
80793adant3 1101 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
81123ad2antl1 1243 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
82303adantr3 1242 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
83823adant3 1101 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8483r19.21bi 2961 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
85323adantr3 1242 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
86853adant3 1101 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
8786r19.21bi 2961 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
8881, 84, 87, 34syl3anc 1366 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
8993ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑆𝑊)
90103ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐼𝑋)
91233ad2ant1 1102 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 𝑅𝑍)
92 simp23 1116 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐵)
935, 1, 89, 90, 91, 6, 92prdsbascl 16190 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑥) ∈ 𝑉)
9493r19.21bi 2961 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝑉)
95 xmetcl 22183 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
9681, 94, 84, 95syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
97 simp3l 1109 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ ℝ)
9897adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) ∈ ℝ)
99 xmetge0 22196 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
10081, 94, 84, 99syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
101 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥)))
10296, 101fmptd 6425 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ*)
103 frn 6091 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
10540a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ∈ ℝ*)
106105snssd 4372 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → {0} ⊆ ℝ*)
107104, 106unssd 3822 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
108107adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
109 ssun1 3809 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})
110 ovex 6718 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑓𝑥)) ∈ V
111110elabrex 6541 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
112111adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
113101rnmpt 5403 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))}
114112, 113syl6eleqr 2741 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))))
115109, 114sseldi 3634 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}))
116 supxrub 12192 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
117108, 115, 116syl2anc 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
118 simp21 1114 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑓𝐵)
1195, 1, 89, 90, 91, 92, 118, 6, 7, 8prdsdsval3 16192 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
120119adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
121117, 120breqtrrd 4713 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))
122 xrrege0 12043 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ* ∧ (𝐷𝑓) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑓𝑥)) ∧ ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
12396, 98, 100, 121, 122syl22anc 1367 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
124 xmetcl 22183 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
12581, 94, 87, 124syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
126 simp3r 1110 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ ℝ)
127126adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) ∈ ℝ)
128 xmetge0 22196 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
12981, 94, 87, 128syl3anc 1366 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
130 eqid 2651 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥)))
131125, 130fmptd 6425 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
132 frn 6091 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
133131, 132syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
134133, 106unssd 3822 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
135134adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
136 ssun1 3809 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})
137 ovex 6718 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑔𝑥)) ∈ V
138137elabrex 6541 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
139138adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
140130rnmpt 5403 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))}
141139, 140syl6eleqr 2741 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))))
142136, 141sseldi 3634 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}))
143 supxrub 12192 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
144135, 142, 143syl2anc 694 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
145 simp22 1115 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑔𝐵)
1465, 1, 89, 90, 91, 92, 145, 6, 7, 8prdsdsval3 16192 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
147146adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
148144, 147breqtrrd 4713 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))
149 xrrege0 12043 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (𝐷𝑔) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑔𝑥)) ∧ ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
150125, 127, 129, 148, 149syl22anc 1367 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
151123, 150readdcld 10107 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ)
15281, 84, 87, 59syl3anc 1366 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
153 xmettri2 22192 . . . . . . . . . . 11 ((𝐸 ∈ (∞Met‘𝑉) ∧ ((𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
15481, 94, 84, 87, 153syl13anc 1368 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
155 rexadd 12101 . . . . . . . . . . 11 ((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
156123, 150, 155syl2anc 694 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
157154, 156breqtrd 4711 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
158 xrrege0 12043 . . . . . . . . 9 (((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ) ∧ (0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
15988, 151, 152, 157, 158syl22anc 1367 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
160 readdcl 10057 . . . . . . . . . 10 (((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
1611603ad2ant3 1104 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
162161adantr 480 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
163123, 150, 98, 127, 121, 148le2addd 10684 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ≤ ((𝐷𝑓) + (𝐷𝑔)))
164159, 151, 162, 157, 163letrd 10232 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
165164ralrimiva 2995 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
16688ralrimiva 2995 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
167 breq1 4688 . . . . . . . 8 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
16836, 167ralrnmpt 6408 . . . . . . 7 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
169166, 168syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
170165, 169mpbird 247 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
171133ad2ant1 1102 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
172171, 92, 118fovrnd 6848 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ (0[,]+∞))
173 elxrge0 12319 . . . . . . . . 9 ((𝐷𝑓) ∈ (0[,]+∞) ↔ ((𝐷𝑓) ∈ ℝ* ∧ 0 ≤ (𝐷𝑓)))
174173simprbi 479 . . . . . . . 8 ((𝐷𝑓) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑓))
175172, 174syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑓))
176171, 92, 145fovrnd 6848 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ (0[,]+∞))
177 elxrge0 12319 . . . . . . . . 9 ((𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝐷𝑔)))
178177simprbi 479 . . . . . . . 8 ((𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑔))
179176, 178syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑔))
18097, 126, 175, 179addge0d 10641 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
181 breq1 4688 . . . . . . 7 (𝑧 = 0 → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔))))
18247, 181ralsn 4254 . . . . . 6 (∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
183180, 182sylibr 224 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
184 ralunb 3827 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ∧ ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
185170, 183, 184sylanbrc 699 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
186433adantr3 1242 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
1871863adant3 1101 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
188161rexrd 10127 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*)
189 supxrleub 12194 . . . . 5 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
190187, 188, 189syl2anc 694 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
191185, 190mpbird 247 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)))
19280, 191eqbrtrd 4707 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) ≤ ((𝐷𝑓) + (𝐷𝑔)))
1934, 16, 20, 78, 192isxmet2d 22179 1 (𝜑𝐷 ∈ (∞Met‘𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  {csn 4210   class class class wbr 4685  cmpt 4762   × cxp 5141  ran crn 5144  cres 5145   Fn wfn 5921  wf 5922  cfv 5926  (class class class)co 6690  supcsup 8387  cr 9973  0cc0 9974   + caddc 9977  +∞cpnf 10109  *cxr 10111   < clt 10112  cle 10113   +𝑒 cxad 11982  [,]cicc 12216  Basecbs 15904  distcds 15997  Xscprds 16153  ∞Metcxmt 19779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-icc 12220  df-fz 12365  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-plusg 16001  df-mulr 16002  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-hom 16013  df-cco 16014  df-prds 16155  df-xmet 19787
This theorem is referenced by:  prdsxmet  22221
  Copyright terms: Public domain W3C validator