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

Theorem isxmet2d 22923
Description: It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: 𝐷(𝑥, 𝑦) = if(𝑥 = 𝑦, 0, -∞) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
Hypotheses
Ref Expression
isxmetd.0 (𝜑𝑋𝑉)
isxmetd.1 (𝜑𝐷:(𝑋 × 𝑋)⟶ℝ*)
isxmet2d.2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 0 ≤ (𝑥𝐷𝑦))
isxmet2d.3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
isxmet2d.4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
Assertion
Ref Expression
isxmet2d (𝜑𝐷 ∈ (∞Met‘𝑋))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐷   𝜑,𝑥,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧
Allowed substitution hints:   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem isxmet2d
StepHypRef Expression
1 isxmetd.0 . 2 (𝜑𝑋𝑉)
2 isxmetd.1 . 2 (𝜑𝐷:(𝑋 × 𝑋)⟶ℝ*)
32fovrnda 7302 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
4 0xr 10673 . . . 4 0 ∈ ℝ*
5 xrletri3 12533 . . . 4 (((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
63, 4, 5sylancl 589 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
7 isxmet2d.2 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 0 ≤ (𝑥𝐷𝑦))
87biantrud 535 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
9 isxmet2d.3 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
106, 8, 93bitr2d 310 . 2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
11 isxmet2d.4 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
12113expa 1115 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
13 rexadd 12611 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
1413adantl 485 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
1512, 14breqtrrd 5075 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
1615anassrs 471 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
1733adantr3 1168 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
18 pnfge 12511 . . . . . . 7 ((𝑥𝐷𝑦) ∈ ℝ* → (𝑥𝐷𝑦) ≤ +∞)
1917, 18syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ≤ +∞)
2019ad2antrr 725 . . . . 5 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
21 oveq2 7146 . . . . . 6 ((𝑧𝐷𝑦) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) +𝑒 +∞))
222ffnd 6496 . . . . . . . . . . 11 (𝜑𝐷 Fn (𝑋 × 𝑋))
23 elxrge0 12833 . . . . . . . . . . . . 13 ((𝑥𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑥𝐷𝑦)))
243, 7, 23sylanbrc 586 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐷𝑦) ∈ (0[,]+∞))
2524ralrimivva 3185 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞))
26 ffnov 7260 . . . . . . . . . . 11 (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞)))
2722, 25, 26sylanbrc 586 . . . . . . . . . 10 (𝜑𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
2827adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
29 simpr3 1193 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
30 simpr1 1191 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑥𝑋)
3128, 29, 30fovrnd 7303 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ∈ (0[,]+∞))
32 eliccxr 12811 . . . . . . . 8 ((𝑧𝐷𝑥) ∈ (0[,]+∞) → (𝑧𝐷𝑥) ∈ ℝ*)
3331, 32syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ∈ ℝ*)
34 renemnf 10675 . . . . . . 7 ((𝑧𝐷𝑥) ∈ ℝ → (𝑧𝐷𝑥) ≠ -∞)
35 xaddpnf1 12605 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ* ∧ (𝑧𝐷𝑥) ≠ -∞) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
3633, 34, 35syl2an 598 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
3721, 36sylan9eqr 2881 . . . . 5 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
3820, 37breqtrrd 5075 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
39 simpr2 1192 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
4028, 29, 39fovrnd 7303 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ∈ (0[,]+∞))
41 eliccxr 12811 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) → (𝑧𝐷𝑦) ∈ ℝ*)
4240, 41syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ∈ ℝ*)
43 elxrge0 12833 . . . . . . . . . . 11 ((𝑧𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)))
4443simprbi 500 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑦))
4540, 44syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 0 ≤ (𝑧𝐷𝑦))
46 ge0nemnf 12552 . . . . . . . . 9 (((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞)
4742, 45, 46syl2anc 587 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ≠ -∞)
4847a1d 25 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞))
4948necon4bd 3033 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
5049adantr 484 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
5150imp 410 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
5242adantr 484 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑧𝐷𝑦) ∈ ℝ*)
53 elxr 12497 . . . . 5 ((𝑧𝐷𝑦) ∈ ℝ* ↔ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5452, 53sylib 221 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5516, 38, 51, 54mpjao3dan 1428 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
5619adantr 484 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
57 oveq1 7145 . . . . 5 ((𝑧𝐷𝑥) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = (+∞ +𝑒 (𝑧𝐷𝑦)))
58 xaddpnf2 12606 . . . . . 6 (((𝑧𝐷𝑦) ∈ ℝ* ∧ (𝑧𝐷𝑦) ≠ -∞) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
5942, 47, 58syl2anc 587 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
6057, 59sylan9eqr 2881 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
6156, 60breqtrrd 5075 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
62 elxrge0 12833 . . . . . . . . 9 ((𝑧𝐷𝑥) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)))
6362simprbi 500 . . . . . . . 8 ((𝑧𝐷𝑥) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑥))
6431, 63syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 0 ≤ (𝑧𝐷𝑥))
65 ge0nemnf 12552 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)) → (𝑧𝐷𝑥) ≠ -∞)
6633, 64, 65syl2anc 587 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ≠ -∞)
6766a1d 25 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑥) ≠ -∞))
6867necon4bd 3033 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑥) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
6968imp 410 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
70 elxr 12497 . . . 4 ((𝑧𝐷𝑥) ∈ ℝ* ↔ ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
7133, 70sylib 221 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
7255, 61, 69, 71mpjao3dan 1428 . 2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
731, 2, 10, 72isxmetd 22922 1 (𝜑𝐷 ∈ (∞Met‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3o 1083  w3a 1084   = wceq 1538  wcel 2115  wne 3013  wral 3132   class class class wbr 5047   × cxp 5534   Fn wfn 6331  wf 6332  cfv 6336  (class class class)co 7138  cr 10521  0cc0 10522   + caddc 10525  +∞cpnf 10657  -∞cmnf 10658  *cxr 10659  cle 10661   +𝑒 cxad 12491  [,]cicc 12727  ∞Metcxmet 20516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-i2m1 10590  ax-rnegex 10593  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-po 5455  df-so 5456  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7141  df-oprab 7142  df-mpo 7143  df-1st 7672  df-2nd 7673  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-xadd 12494  df-icc 12731  df-xmet 20524
This theorem is referenced by:  prdsxmetlem  22964  xrsxmet  23403
  Copyright terms: Public domain W3C validator