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

Theorem prdsxmetlem 21983
 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 6113 . . . 4 (Base‘𝑌) ∈ V
31, 2eqeltri 2684 . . 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 21982 . . 3 (𝜑𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
14 iccssxr 12127 . . 3 (0[,]+∞) ⊆ ℝ*
15 fss 5969 . . 3 ((𝐷:(𝐵 × 𝐵)⟶(0[,]+∞) ∧ (0[,]+∞) ⊆ ℝ*) → 𝐷:(𝐵 × 𝐵)⟶ℝ*)
1613, 14, 15sylancl 693 . 2 (𝜑𝐷:(𝐵 × 𝐵)⟶ℝ*)
1713fovrnda 6703 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) ∈ (0[,]+∞))
18 elxrge0 12152 . . . 4 ((𝑓𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝑓𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐷𝑔)))
1918simprbi 479 . . 3 ((𝑓𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝑓𝐷𝑔))
2017, 19syl 17 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ≤ (𝑓𝐷𝑔))
219adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑆𝑊)
2210adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝐼𝑋)
2311ralrimiva 2949 . . . . . 6 (𝜑 → ∀𝑥𝐼 𝑅𝑍)
2423adantr 480 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 𝑅𝑍)
25 simprl 790 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓𝐵)
26 simprr 792 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔𝐵)
275, 1, 21, 22, 24, 25, 26, 6, 7, 8prdsdsval3 15968 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
2827breq1d 4593 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ 0))
2912adantlr 747 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
305, 1, 21, 22, 24, 6, 25prdsbascl 15966 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
3130r19.21bi 2916 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
325, 1, 21, 22, 24, 6, 26prdsbascl 15966 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
3332r19.21bi 2916 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
34 xmetcl 21946 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
3529, 31, 33, 34syl3anc 1318 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
36 eqid 2610 . . . . . . 7 (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))
3735, 36fmptd 6292 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
38 frn 5966 . . . . . 6 ((𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
3937, 38syl 17 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
40 0xr 9965 . . . . . . 7 0 ∈ ℝ*
4140a1i 11 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 0 ∈ ℝ*)
4241snssd 4281 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → {0} ⊆ ℝ*)
4339, 42unssd 3751 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
44 supxrleub 12028 . . . 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 10987 . . . . . . 7 0 ≤ 0
47 c0ex 9913 . . . . . . . 8 0 ∈ V
48 breq1 4586 . . . . . . . 8 (𝑧 = 0 → (𝑧 ≤ 0 ↔ 0 ≤ 0))
4947, 48ralsn 4169 . . . . . . 7 (∀𝑧 ∈ {0}𝑧 ≤ 0 ↔ 0 ≤ 0)
5046, 49mpbir 220 . . . . . 6 𝑧 ∈ {0}𝑧 ≤ 0
51 ralunb 3756 . . . . . 6 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ∧ ∀𝑧 ∈ {0}𝑧 ≤ 0))
5250, 51mpbiran2 956 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0)
53 ovex 6577 . . . . . . 7 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
5453rgenw 2908 . . . . . 6 𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V
55 breq1 4586 . . . . . . 7 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ 0 ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5636, 55ralrnmpt 6276 . . . . . 6 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ V → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0))
5754, 56ax-mp 5 . . . . 5 (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
5852, 57bitri 263 . . . 4 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0)
59 xmetge0 21959 . . . . . . . . 9 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6029, 31, 33, 59syl3anc 1318 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
6160biantrud 527 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
62 xrletri3 11861 . . . . . . . 8 ((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ 0 ∈ ℝ*) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
6335, 40, 62sylancl 693 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ∧ 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))))
64 xmeteq0 21953 . . . . . . . 8 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6529, 31, 33, 64syl3anc 1318 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) = 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6661, 63, 653bitr2d 295 . . . . . 6 (((𝜑 ∧ (𝑓𝐵𝑔𝐵)) ∧ 𝑥𝐼) → (((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ (𝑓𝑥) = (𝑔𝑥)))
6766ralbidva 2968 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
68 eqid 2610 . . . . . . . . . 10 (𝑥𝐼𝑅) = (𝑥𝐼𝑅)
6968fnmpt 5933 . . . . . . . . 9 (∀𝑥𝐼 𝑅𝑍 → (𝑥𝐼𝑅) Fn 𝐼)
7023, 69syl 17 . . . . . . . 8 (𝜑 → (𝑥𝐼𝑅) Fn 𝐼)
7170adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑥𝐼𝑅) Fn 𝐼)
725, 1, 21, 22, 71, 25prdsbasfn 15954 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑓 Fn 𝐼)
735, 1, 21, 22, 71, 26prdsbasfn 15954 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → 𝑔 Fn 𝐼)
74 eqfnfv 6219 . . . . . 6 ((𝑓 Fn 𝐼𝑔 Fn 𝐼) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7572, 73, 74syl2anc 691 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (𝑓 = 𝑔 ↔ ∀𝑥𝐼 (𝑓𝑥) = (𝑔𝑥)))
7667, 75bitr4d 270 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ 0 ↔ 𝑓 = 𝑔))
7758, 76syl5bb 271 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ 0 ↔ 𝑓 = 𝑔))
7828, 45, 773bitrd 293 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵)) → ((𝑓𝐷𝑔) ≤ 0 ↔ 𝑓 = 𝑔))
79273adantr3 1215 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
80793adant3 1074 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
81123ad2antl1 1216 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 𝐸 ∈ (∞Met‘𝑉))
82303adantr3 1215 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
83823adant3 1074 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑓𝑥) ∈ 𝑉)
8483r19.21bi 2916 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑓𝑥) ∈ 𝑉)
85323adantr3 1215 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
86853adant3 1074 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑔𝑥) ∈ 𝑉)
8786r19.21bi 2916 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑔𝑥) ∈ 𝑉)
8881, 84, 87, 34syl3anc 1318 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
8993ad2ant1 1075 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑆𝑊)
90103ad2ant1 1075 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐼𝑋)
91233ad2ant1 1075 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 𝑅𝑍)
92 simp23 1089 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐵)
935, 1, 89, 90, 91, 6, 92prdsbascl 15966 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 (𝑥) ∈ 𝑉)
9493r19.21bi 2916 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝑥) ∈ 𝑉)
95 xmetcl 21946 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
9681, 94, 84, 95syl3anc 1318 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ*)
97 simp3l 1082 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ ℝ)
9897adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) ∈ ℝ)
99 xmetge0 21959 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
10081, 94, 84, 99syl3anc 1318 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑓𝑥)))
101 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥)))
10296, 101fmptd 6292 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ*)
103 frn 5966 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
104102, 103syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ ℝ*)
10540a1i 11 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ∈ ℝ*)
106105snssd 4281 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → {0} ⊆ ℝ*)
107104, 106unssd 3751 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
108107adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ*)
109 ssun1 3738 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})
110 ovex 6577 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑓𝑥)) ∈ V
111110elabrex 6405 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
112111adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))})
113101rnmpt 5292 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑓𝑥))}
114112, 113syl6eleqr 2699 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))))
115109, 114sseldi 3566 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}))
116 supxrub 12026 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑓𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
117108, 115, 116syl2anc 691 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
118 simp21 1087 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑓𝐵)
1195, 1, 89, 90, 91, 92, 118, 6, 7, 8prdsdsval3 15968 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
120119adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑓) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑓𝑥))) ∪ {0}), ℝ*, < ))
121117, 120breqtrrd 4611 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))
122 xrrege0 11879 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ* ∧ (𝐷𝑓) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑓𝑥)) ∧ ((𝑥)𝐸(𝑓𝑥)) ≤ (𝐷𝑓))) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
12396, 98, 100, 121, 122syl22anc 1319 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑓𝑥)) ∈ ℝ)
124 xmetcl 21946 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
12581, 94, 87, 124syl3anc 1318 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
126 simp3r 1083 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ ℝ)
127126adantr 480 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) ∈ ℝ)
128 xmetge0 21959 . . . . . . . . . . . 12 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
12981, 94, 87, 128syl3anc 1318 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑥)𝐸(𝑔𝑥)))
130 eqid 2610 . . . . . . . . . . . . . . . . 17 (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥)))
131125, 130fmptd 6292 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ*)
132 frn 5966 . . . . . . . . . . . . . . . 16 ((𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))):𝐼⟶ℝ* → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
133131, 132syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ ℝ*)
134133, 106unssd 3751 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
135134adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
136 ssun1 3738 . . . . . . . . . . . . . 14 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ⊆ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})
137 ovex 6577 . . . . . . . . . . . . . . . . 17 ((𝑥)𝐸(𝑔𝑥)) ∈ V
138137elabrex 6405 . . . . . . . . . . . . . . . 16 (𝑥𝐼 → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
139138adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))})
140130rnmpt 5292 . . . . . . . . . . . . . . 15 ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) = {𝑧 ∣ ∃𝑥𝐼 𝑧 = ((𝑥)𝐸(𝑔𝑥))}
141139, 140syl6eleqr 2699 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))))
142136, 141sseldi 3566 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}))
143 supxrub 12026 . . . . . . . . . . . . 13 (((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ (ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0})) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
144135, 142, 143syl2anc 691 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
145 simp22 1088 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝑔𝐵)
1465, 1, 89, 90, 91, 92, 145, 6, 7, 8prdsdsval3 15968 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
147146adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (𝐷𝑔) = sup((ran (𝑥𝐼 ↦ ((𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ))
148144, 147breqtrrd 4611 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))
149 xrrege0 11879 . . . . . . . . . . 11 (((((𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (𝐷𝑔) ∈ ℝ) ∧ (0 ≤ ((𝑥)𝐸(𝑔𝑥)) ∧ ((𝑥)𝐸(𝑔𝑥)) ≤ (𝐷𝑔))) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
150125, 127, 129, 148, 149syl22anc 1319 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
151123, 150readdcld 9948 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ)
15281, 84, 87, 59syl3anc 1318 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → 0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)))
153 xmettri2 21955 . . . . . . . . . . 11 ((𝐸 ∈ (∞Met‘𝑉) ∧ ((𝑥) ∈ 𝑉 ∧ (𝑓𝑥) ∈ 𝑉 ∧ (𝑔𝑥) ∈ 𝑉)) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
15481, 94, 84, 87, 153syl13anc 1320 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))))
155 rexadd 11937 . . . . . . . . . . 11 ((((𝑥)𝐸(𝑓𝑥)) ∈ ℝ ∧ ((𝑥)𝐸(𝑔𝑥)) ∈ ℝ) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
156123, 150, 155syl2anc 691 . . . . . . . . . 10 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) +𝑒 ((𝑥)𝐸(𝑔𝑥))) = (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
157154, 156breqtrd 4609 . . . . . . . . 9 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))
158 xrrege0 11879 . . . . . . . . 9 (((((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* ∧ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ∈ ℝ) ∧ (0 ≤ ((𝑓𝑥)𝐸(𝑔𝑥)) ∧ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))))) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
15988, 151, 152, 157, 158syl22anc 1319 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ)
160 readdcl 9898 . . . . . . . . . 10 (((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
1611603ad2ant3 1077 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
162161adantr 480 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ)
163123, 150, 98, 127, 121, 148le2addd 10525 . . . . . . . 8 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → (((𝑥)𝐸(𝑓𝑥)) + ((𝑥)𝐸(𝑔𝑥))) ≤ ((𝐷𝑓) + (𝐷𝑔)))
164159, 151, 162, 157, 163letrd 10073 . . . . . . 7 (((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) ∧ 𝑥𝐼) → ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
165164ralrimiva 2949 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔)))
16688ralrimiva 2949 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ*)
167 breq1 4586 . . . . . . . 8 (𝑧 = ((𝑓𝑥)𝐸(𝑔𝑥)) → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
16836, 167ralrnmpt 6276 . . . . . . 7 (∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ∈ ℝ* → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
169166, 168syl 17 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑥𝐼 ((𝑓𝑥)𝐸(𝑔𝑥)) ≤ ((𝐷𝑓) + (𝐷𝑔))))
170165, 169mpbird 246 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
171133ad2ant1 1075 . . . . . . . . 9 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 𝐷:(𝐵 × 𝐵)⟶(0[,]+∞))
172171, 92, 118fovrnd 6704 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑓) ∈ (0[,]+∞))
173 elxrge0 12152 . . . . . . . . 9 ((𝐷𝑓) ∈ (0[,]+∞) ↔ ((𝐷𝑓) ∈ ℝ* ∧ 0 ≤ (𝐷𝑓)))
174173simprbi 479 . . . . . . . 8 ((𝐷𝑓) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑓))
175172, 174syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑓))
176171, 92, 145fovrnd 6704 . . . . . . . 8 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝐷𝑔) ∈ (0[,]+∞))
177 elxrge0 12152 . . . . . . . . 9 ((𝐷𝑔) ∈ (0[,]+∞) ↔ ((𝐷𝑔) ∈ ℝ* ∧ 0 ≤ (𝐷𝑔)))
178177simprbi 479 . . . . . . . 8 ((𝐷𝑔) ∈ (0[,]+∞) → 0 ≤ (𝐷𝑔))
179176, 178syl 17 . . . . . . 7 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ (𝐷𝑔))
18097, 126, 175, 179addge0d 10482 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
181 breq1 4586 . . . . . . 7 (𝑧 = 0 → (𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔))))
18247, 181ralsn 4169 . . . . . 6 (∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ 0 ≤ ((𝐷𝑓) + (𝐷𝑔)))
183180, 182sylibr 223 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
184 ralunb 3756 . . . . 5 (∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ (∀𝑧 ∈ ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥)))𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)) ∧ ∀𝑧 ∈ {0}𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
185170, 183, 184sylanbrc 695 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔)))
186433adantr3 1215 . . . . . 6 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
1871863adant3 1074 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ*)
188161rexrd 9968 . . . . 5 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*)
189 supxrleub 12028 . . . . 5 (((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}) ⊆ ℝ* ∧ ((𝐷𝑓) + (𝐷𝑔)) ∈ ℝ*) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
190187, 188, 189syl2anc 691 . . . 4 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)) ↔ ∀𝑧 ∈ (ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0})𝑧 ≤ ((𝐷𝑓) + (𝐷𝑔))))
191185, 190mpbird 246 . . 3 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → sup((ran (𝑥𝐼 ↦ ((𝑓𝑥)𝐸(𝑔𝑥))) ∪ {0}), ℝ*, < ) ≤ ((𝐷𝑓) + (𝐷𝑔)))
19280, 191eqbrtrd 4605 . 2 ((𝜑 ∧ (𝑓𝐵𝑔𝐵𝐵) ∧ ((𝐷𝑓) ∈ ℝ ∧ (𝐷𝑔) ∈ ℝ)) → (𝑓𝐷𝑔) ≤ ((𝐷𝑓) + (𝐷𝑔)))
1934, 16, 20, 78, 192isxmet2d 21942 1 (𝜑𝐷 ∈ (∞Met‘𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ran crn 5039   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  supcsup 8229  ℝcr 9814  0cc0 9815   + caddc 9818  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   +𝑒 cxad 11820  [,]cicc 12049  Basecbs 15695  distcds 15777  Xscprds 15929  ∞Metcxmt 19552 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-icc 12053  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-sca 15784  df-vsca 15785  df-ip 15786  df-tset 15787  df-ple 15788  df-ds 15791  df-hom 15793  df-cco 15794  df-prds 15931  df-xmet 19560 This theorem is referenced by:  prdsxmet  21984
 Copyright terms: Public domain W3C validator