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 φXV
isxmetd.1 φD:X×X*
isxmet2d.2 φxXyX0xDy
isxmet2d.3 φxXyXxDy0x=y
isxmet2d.4 φxXyXzXzDxzDyxDyzDx+zDy
Assertion isxmet2d φD∞MetX

Proof

Step Hyp Ref Expression
1 isxmetd.0 φXV
2 isxmetd.1 φD:X×X*
3 isxmet2d.2 φxXyX0xDy
4 isxmet2d.3 φxXyXxDy0x=y
5 isxmet2d.4 φxXyXzXzDxzDyxDyzDx+zDy
6 2 fovrnda φxXyXxDy*
7 0xr 0*
8 xrletri3 xDy*0*xDy=0xDy00xDy
9 6 7 8 sylancl φxXyXxDy=0xDy00xDy
10 3 biantrud φxXyXxDy0xDy00xDy
11 9 10 4 3bitr2d φxXyXxDy=0x=y
12 5 3expa φxXyXzXzDxzDyxDyzDx+zDy
13 rexadd zDxzDyzDx+𝑒zDy=zDx+zDy
14 13 adantl φxXyXzXzDxzDyzDx+𝑒zDy=zDx+zDy
15 12 14 breqtrrd φxXyXzXzDxzDyxDyzDx+𝑒zDy
16 15 anassrs φxXyXzXzDxzDyxDyzDx+𝑒zDy
17 6 3adantr3 φxXyXzXxDy*
18 pnfge xDy*xDy+∞
19 17 18 syl φxXyXzXxDy+∞
20 19 ad2antrr φxXyXzXzDxzDy=+∞xDy+∞
21 oveq2 zDy=+∞zDx+𝑒zDy=zDx+𝑒+∞
22 2 ffnd φDFnX×X
23 elxrge0 xDy0+∞xDy*0xDy
24 6 3 23 sylanbrc φxXyXxDy0+∞
25 24 ralrimivva φxXyXxDy0+∞
26 ffnov D:X×X0+∞DFnX×XxXyXxDy0+∞
27 22 25 26 sylanbrc φD:X×X0+∞
28 27 adantr φxXyXzXD:X×X0+∞
29 simpr3 φxXyXzXzX
30 simpr1 φxXyXzXxX
31 28 29 30 fovrnd φxXyXzXzDx0+∞
32 eliccxr zDx0+∞zDx*
33 31 32 syl φxXyXzXzDx*
34 renemnf zDxzDx−∞
35 xaddpnf1 zDx*zDx−∞zDx+𝑒+∞=+∞
36 33 34 35 syl2an φxXyXzXzDxzDx+𝑒+∞=+∞
37 21 36 sylan9eqr φxXyXzXzDxzDy=+∞zDx+𝑒zDy=+∞
38 20 37 breqtrrd φxXyXzXzDxzDy=+∞xDyzDx+𝑒zDy
39 simpr2 φxXyXzXyX
40 28 29 39 fovrnd φxXyXzXzDy0+∞
41 eliccxr zDy0+∞zDy*
42 40 41 syl φxXyXzXzDy*
43 elxrge0 zDy0+∞zDy*0zDy
44 43 simprbi zDy0+∞0zDy
45 40 44 syl φxXyXzX0zDy
46 ge0nemnf zDy*0zDyzDy−∞
47 42 45 46 syl2anc φxXyXzXzDy−∞
48 47 a1d φxXyXzX¬xDyzDx+𝑒zDyzDy−∞
49 48 necon4bd φxXyXzXzDy=−∞xDyzDx+𝑒zDy
50 49 adantr φxXyXzXzDxzDy=−∞xDyzDx+𝑒zDy
51 50 imp φxXyXzXzDxzDy=−∞xDyzDx+𝑒zDy
52 42 adantr φxXyXzXzDxzDy*
53 elxr zDy*zDyzDy=+∞zDy=−∞
54 52 53 sylib φxXyXzXzDxzDyzDy=+∞zDy=−∞
55 16 38 51 54 mpjao3dan φxXyXzXzDxxDyzDx+𝑒zDy
56 19 adantr φxXyXzXzDx=+∞xDy+∞
57 oveq1 zDx=+∞zDx+𝑒zDy=+∞+𝑒zDy
58 xaddpnf2 zDy*zDy−∞+∞+𝑒zDy=+∞
59 42 47 58 syl2anc φxXyXzX+∞+𝑒zDy=+∞
60 57 59 sylan9eqr φxXyXzXzDx=+∞zDx+𝑒zDy=+∞
61 56 60 breqtrrd φxXyXzXzDx=+∞xDyzDx+𝑒zDy
62 elxrge0 zDx0+∞zDx*0zDx
63 62 simprbi zDx0+∞0zDx
64 31 63 syl φxXyXzX0zDx
65 ge0nemnf zDx*0zDxzDx−∞
66 33 64 65 syl2anc φxXyXzXzDx−∞
67 66 a1d φxXyXzX¬xDyzDx+𝑒zDyzDx−∞
68 67 necon4bd φxXyXzXzDx=−∞xDyzDx+𝑒zDy
69 68 imp φxXyXzXzDx=−∞xDyzDx+𝑒zDy
70 elxr zDx*zDxzDx=+∞zDx=−∞
71 33 70 sylib φxXyXzXzDxzDx=+∞zDx=−∞
72 55 61 69 71 mpjao3dan φxXyXzXxDyzDx+𝑒zDy
73 1 2 11 72 isxmetd φD∞MetX