Metamath Proof Explorer


Theorem isxmet2d

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: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses isxmetd.0 ( 𝜑𝑋𝑉 )
isxmetd.1 ( 𝜑𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
isxmet2d.2 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
isxmet2d.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
isxmet2d.4 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
Assertion isxmet2d ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 isxmetd.0 ( 𝜑𝑋𝑉 )
2 isxmetd.1 ( 𝜑𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 isxmet2d.2 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
4 isxmet2d.3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ 𝑥 = 𝑦 ) )
5 isxmet2d.4 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
6 2 fovrnda ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
7 0xr 0 ∈ ℝ*
8 xrletri3 ( ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
9 6 7 8 sylancl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
10 3 biantrud ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ↔ ( ( 𝑥 𝐷 𝑦 ) ≤ 0 ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) ) )
11 9 10 4 3bitr2d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( ( 𝑥 𝐷 𝑦 ) = 0 ↔ 𝑥 = 𝑦 ) )
12 5 3expa ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
13 rexadd ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
14 13 adantl ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) + ( 𝑧 𝐷 𝑦 ) ) )
15 12 14 breqtrrd ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
16 15 anassrs ( ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
17 6 3adantr3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
18 pnfge ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
19 17 18 syl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
20 19 ad2antrr ( ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
21 oveq2 ( ( 𝑧 𝐷 𝑦 ) = +∞ → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) )
22 2 ffnd ( 𝜑𝐷 Fn ( 𝑋 × 𝑋 ) )
23 elxrge0 ( ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑥 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
24 6 3 23 sylanbrc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
25 24 ralrimivva ( 𝜑 → ∀ 𝑥𝑋𝑦𝑋 ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
26 ffnov ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) ↔ ( 𝐷 Fn ( 𝑋 × 𝑋 ) ∧ ∀ 𝑥𝑋𝑦𝑋 ( 𝑥 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ) )
27 22 25 26 sylanbrc ( 𝜑𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )
28 27 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )
29 simpr3 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 𝑧𝑋 )
30 simpr1 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 𝑥𝑋 )
31 28 29 30 fovrnd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) )
32 eliccxr ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ* )
33 31 32 syl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ∈ ℝ* )
34 renemnf ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
35 xaddpnf1 ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ ( 𝑧 𝐷 𝑥 ) ≠ -∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) = +∞ )
36 33 34 35 syl2an ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 +∞ ) = +∞ )
37 21 36 sylan9eqr ( ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
38 20 37 breqtrrd ( ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
39 simpr2 ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 𝑦𝑋 )
40 28 29 39 fovrnd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) )
41 eliccxr ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
42 40 41 syl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
43 elxrge0 ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑦 ) ) )
44 43 simprbi ( ( 𝑧 𝐷 𝑦 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑧 𝐷 𝑦 ) )
45 40 44 syl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 0 ≤ ( 𝑧 𝐷 𝑦 ) )
46 ge0nemnf ( ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ )
47 42 45 46 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ )
48 47 a1d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( ¬ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑦 ) ≠ -∞ ) )
49 48 necon4bd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( ( 𝑧 𝐷 𝑦 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
50 49 adantr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑦 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
51 50 imp ( ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) ∧ ( 𝑧 𝐷 𝑦 ) = -∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
52 42 adantr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( 𝑧 𝐷 𝑦 ) ∈ ℝ* )
53 elxr ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ↔ ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑦 ) = +∞ ∨ ( 𝑧 𝐷 𝑦 ) = -∞ ) )
54 52 53 sylib ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑦 ) = +∞ ∨ ( 𝑧 𝐷 𝑦 ) = -∞ ) )
55 16 38 51 54 mpjao3dan ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) ∈ ℝ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
56 19 adantr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ +∞ )
57 oveq1 ( ( 𝑧 𝐷 𝑥 ) = +∞ → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
58 xaddpnf2 ( ( ( 𝑧 𝐷 𝑦 ) ∈ ℝ* ∧ ( 𝑧 𝐷 𝑦 ) ≠ -∞ ) → ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
59 42 47 58 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( +∞ +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
60 57 59 sylan9eqr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) = +∞ )
61 56 60 breqtrrd ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = +∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
62 elxrge0 ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑥 ) ) )
63 62 simprbi ( ( 𝑧 𝐷 𝑥 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑧 𝐷 𝑥 ) )
64 31 63 syl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → 0 ≤ ( 𝑧 𝐷 𝑥 ) )
65 ge0nemnf ( ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑥 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
66 33 64 65 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ )
67 66 a1d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( ¬ ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) → ( 𝑧 𝐷 𝑥 ) ≠ -∞ ) )
68 67 necon4bd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) = -∞ → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) ) )
69 68 imp ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) ∧ ( 𝑧 𝐷 𝑥 ) = -∞ ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
70 elxr ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ* ↔ ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑥 ) = +∞ ∨ ( 𝑧 𝐷 𝑥 ) = -∞ ) )
71 33 70 sylib ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( ( 𝑧 𝐷 𝑥 ) ∈ ℝ ∨ ( 𝑧 𝐷 𝑥 ) = +∞ ∨ ( 𝑧 𝐷 𝑥 ) = -∞ ) )
72 55 61 69 71 mpjao3dan ( ( 𝜑 ∧ ( 𝑥𝑋𝑦𝑋𝑧𝑋 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( ( 𝑧 𝐷 𝑥 ) +𝑒 ( 𝑧 𝐷 𝑦 ) ) )
73 1 2 11 72 isxmetd ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )