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

Theorem isxmet2d 23680
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 (𝜑𝐷:(𝑋 × 𝑋)⟶ℝ*)
32fovcdmda 7525 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
4 0xr 11202 . . . 4 0 ∈ ℝ*
5 xrletri3 13073 . . . 4 (((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ∈ ℝ*) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
63, 4, 5sylancl 586 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
7 isxmet2d.2 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 0 ≤ (𝑥𝐷𝑦))
87biantrud 532 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ ((𝑥𝐷𝑦) ≤ 0 ∧ 0 ≤ (𝑥𝐷𝑦))))
9 isxmet2d.3 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) ≤ 0 ↔ 𝑥 = 𝑦))
106, 8, 93bitr2d 306 . 2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑥𝐷𝑦) = 0 ↔ 𝑥 = 𝑦))
11 isxmet2d.4 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
12113expa 1118 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
13 rexadd 13151 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
1413adantl 482 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) + (𝑧𝐷𝑦)))
1512, 14breqtrrd 5133 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ ((𝑧𝐷𝑥) ∈ ℝ ∧ (𝑧𝐷𝑦) ∈ ℝ)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
1615anassrs 468 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
1733adantr3 1171 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ∈ ℝ*)
18 pnfge 13051 . . . . . . 7 ((𝑥𝐷𝑦) ∈ ℝ* → (𝑥𝐷𝑦) ≤ +∞)
1917, 18syl 17 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ≤ +∞)
2019ad2antrr 724 . . . . 5 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
21 oveq2 7365 . . . . . 6 ((𝑧𝐷𝑦) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = ((𝑧𝐷𝑥) +𝑒 +∞))
222ffnd 6669 . . . . . . . . . . 11 (𝜑𝐷 Fn (𝑋 × 𝑋))
23 elxrge0 13374 . . . . . . . . . . . . 13 ((𝑥𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑥𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑥𝐷𝑦)))
243, 7, 23sylanbrc 583 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝐷𝑦) ∈ (0[,]+∞))
2524ralrimivva 3197 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝑋𝑦𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞))
26 ffnov 7483 . . . . . . . . . . 11 (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑥𝑋𝑦𝑋 (𝑥𝐷𝑦) ∈ (0[,]+∞)))
2722, 25, 26sylanbrc 583 . . . . . . . . . 10 (𝜑𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
2827adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
29 simpr3 1196 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑧𝑋)
30 simpr1 1194 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑥𝑋)
3128, 29, 30fovcdmd 7526 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ∈ (0[,]+∞))
32 eliccxr 13352 . . . . . . . 8 ((𝑧𝐷𝑥) ∈ (0[,]+∞) → (𝑧𝐷𝑥) ∈ ℝ*)
3331, 32syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ∈ ℝ*)
34 renemnf 11204 . . . . . . 7 ((𝑧𝐷𝑥) ∈ ℝ → (𝑧𝐷𝑥) ≠ -∞)
35 xaddpnf1 13145 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ* ∧ (𝑧𝐷𝑥) ≠ -∞) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
3633, 34, 35syl2an 596 . . . . . 6 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑥) +𝑒 +∞) = +∞)
3721, 36sylan9eqr 2798 . . . . 5 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
3820, 37breqtrrd 5133 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
39 simpr2 1195 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 𝑦𝑋)
4028, 29, 39fovcdmd 7526 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ∈ (0[,]+∞))
41 eliccxr 13352 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) → (𝑧𝐷𝑦) ∈ ℝ*)
4240, 41syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ∈ ℝ*)
43 elxrge0 13374 . . . . . . . . . . 11 ((𝑧𝐷𝑦) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)))
4443simprbi 497 . . . . . . . . . 10 ((𝑧𝐷𝑦) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑦))
4540, 44syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 0 ≤ (𝑧𝐷𝑦))
46 ge0nemnf 13092 . . . . . . . . 9 (((𝑧𝐷𝑦) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞)
4742, 45, 46syl2anc 584 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑦) ≠ -∞)
4847a1d 25 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑦) ≠ -∞))
4948necon4bd 2963 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
5049adantr 481 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
5150imp 407 . . . 4 ((((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) ∧ (𝑧𝐷𝑦) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
5242adantr 481 . . . . 5 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑧𝐷𝑦) ∈ ℝ*)
53 elxr 13037 . . . . 5 ((𝑧𝐷𝑦) ∈ ℝ* ↔ ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5452, 53sylib 217 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → ((𝑧𝐷𝑦) ∈ ℝ ∨ (𝑧𝐷𝑦) = +∞ ∨ (𝑧𝐷𝑦) = -∞))
5516, 38, 51, 54mpjao3dan 1431 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) ∈ ℝ) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
5619adantr 481 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ +∞)
57 oveq1 7364 . . . . 5 ((𝑧𝐷𝑥) = +∞ → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = (+∞ +𝑒 (𝑧𝐷𝑦)))
58 xaddpnf2 13146 . . . . . 6 (((𝑧𝐷𝑦) ∈ ℝ* ∧ (𝑧𝐷𝑦) ≠ -∞) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
5942, 47, 58syl2anc 584 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (+∞ +𝑒 (𝑧𝐷𝑦)) = +∞)
6057, 59sylan9eqr 2798 . . . 4 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) = +∞)
6156, 60breqtrrd 5133 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = +∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
62 elxrge0 13374 . . . . . . . . 9 ((𝑧𝐷𝑥) ∈ (0[,]+∞) ↔ ((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)))
6362simprbi 497 . . . . . . . 8 ((𝑧𝐷𝑥) ∈ (0[,]+∞) → 0 ≤ (𝑧𝐷𝑥))
6431, 63syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → 0 ≤ (𝑧𝐷𝑥))
65 ge0nemnf 13092 . . . . . . 7 (((𝑧𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑧𝐷𝑥)) → (𝑧𝐷𝑥) ≠ -∞)
6633, 64, 65syl2anc 584 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑧𝐷𝑥) ≠ -∞)
6766a1d 25 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (¬ (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)) → (𝑧𝐷𝑥) ≠ -∞))
6867necon4bd 2963 . . . 4 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑥) = -∞ → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦))))
6968imp 407 . . 3 (((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) ∧ (𝑧𝐷𝑥) = -∞) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
70 elxr 13037 . . . 4 ((𝑧𝐷𝑥) ∈ ℝ* ↔ ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
7133, 70sylib 217 . . 3 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → ((𝑧𝐷𝑥) ∈ ℝ ∨ (𝑧𝐷𝑥) = +∞ ∨ (𝑧𝐷𝑥) = -∞))
7255, 61, 69, 71mpjao3dan 1431 . 2 ((𝜑 ∧ (𝑥𝑋𝑦𝑋𝑧𝑋)) → (𝑥𝐷𝑦) ≤ ((𝑧𝐷𝑥) +𝑒 (𝑧𝐷𝑦)))
731, 2, 10, 72isxmetd 23679 1 (𝜑𝐷 ∈ (∞Met‘𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wral 3064   class class class wbr 5105   × cxp 5631   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cr 11050  0cc0 11051   + caddc 11054  +∞cpnf 11186  -∞cmnf 11187  *cxr 11188  cle 11190   +𝑒 cxad 13031  [,]cicc 13267  ∞Metcxmet 20781
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-i2m1 11119  ax-rnegex 11122  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-xadd 13034  df-icc 13271  df-xmet 20789
This theorem is referenced by:  prdsxmetlem  23721  xrsxmet  24172
  Copyright terms: Public domain W3C validator