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 
|- ( ph -> X e. V )
isxmetd.1 
|- ( ph -> D : ( X X. X ) --> RR* )
isxmet2d.2 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x D y ) )
isxmet2d.3 
|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> x = y ) )
isxmet2d.4 
|- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
Assertion isxmet2d 
|- ( ph -> D e. ( *Met ` X ) )

Proof

Step Hyp Ref Expression
1 isxmetd.0 
 |-  ( ph -> X e. V )
2 isxmetd.1 
 |-  ( ph -> D : ( X X. X ) --> RR* )
3 isxmet2d.2 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x D y ) )
4 isxmet2d.3 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> x = y ) )
5 isxmet2d.4 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
6 2 fovrnda 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) e. RR* )
7 0xr 
 |-  0 e. RR*
8 xrletri3 
 |-  ( ( ( x D y ) e. RR* /\ 0 e. RR* ) -> ( ( x D y ) = 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
9 6 7 8 sylancl 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
10 3 biantrud 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
11 9 10 4 3bitr2d 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )
12 5 3expa 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )
13 rexadd 
 |-  ( ( ( z D x ) e. RR /\ ( z D y ) e. RR ) -> ( ( z D x ) +e ( z D y ) ) = ( ( z D x ) + ( z D y ) ) )
14 13 adantl 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( ( z D x ) +e ( z D y ) ) = ( ( z D x ) + ( z D y ) ) )
15 12 14 breqtrrd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
16 15 anassrs 
 |-  ( ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) /\ ( z D y ) e. RR ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
17 6 3adantr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) e. RR* )
18 pnfge 
 |-  ( ( x D y ) e. RR* -> ( x D y ) <_ +oo )
19 17 18 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ +oo )
20 19 ad2antrr 
 |-  ( ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) /\ ( z D y ) = +oo ) -> ( x D y ) <_ +oo )
21 oveq2 
 |-  ( ( z D y ) = +oo -> ( ( z D x ) +e ( z D y ) ) = ( ( z D x ) +e +oo ) )
22 2 ffnd 
 |-  ( ph -> D Fn ( X X. X ) )
23 elxrge0 
 |-  ( ( x D y ) e. ( 0 [,] +oo ) <-> ( ( x D y ) e. RR* /\ 0 <_ ( x D y ) ) )
24 6 3 23 sylanbrc 
 |-  ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) e. ( 0 [,] +oo ) )
25 24 ralrimivva 
 |-  ( ph -> A. x e. X A. y e. X ( x D y ) e. ( 0 [,] +oo ) )
26 ffnov 
 |-  ( D : ( X X. X ) --> ( 0 [,] +oo ) <-> ( D Fn ( X X. X ) /\ A. x e. X A. y e. X ( x D y ) e. ( 0 [,] +oo ) ) )
27 22 25 26 sylanbrc 
 |-  ( ph -> D : ( X X. X ) --> ( 0 [,] +oo ) )
28 27 adantr 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )
29 simpr3 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> z e. X )
30 simpr1 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> x e. X )
31 28 29 30 fovrnd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) e. ( 0 [,] +oo ) )
32 eliccxr 
 |-  ( ( z D x ) e. ( 0 [,] +oo ) -> ( z D x ) e. RR* )
33 31 32 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) e. RR* )
34 renemnf 
 |-  ( ( z D x ) e. RR -> ( z D x ) =/= -oo )
35 xaddpnf1 
 |-  ( ( ( z D x ) e. RR* /\ ( z D x ) =/= -oo ) -> ( ( z D x ) +e +oo ) = +oo )
36 33 34 35 syl2an 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( ( z D x ) +e +oo ) = +oo )
37 21 36 sylan9eqr 
 |-  ( ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) /\ ( z D y ) = +oo ) -> ( ( z D x ) +e ( z D y ) ) = +oo )
38 20 37 breqtrrd 
 |-  ( ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) /\ ( z D y ) = +oo ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
39 simpr2 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> y e. X )
40 28 29 39 fovrnd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) e. ( 0 [,] +oo ) )
41 eliccxr 
 |-  ( ( z D y ) e. ( 0 [,] +oo ) -> ( z D y ) e. RR* )
42 40 41 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) e. RR* )
43 elxrge0 
 |-  ( ( z D y ) e. ( 0 [,] +oo ) <-> ( ( z D y ) e. RR* /\ 0 <_ ( z D y ) ) )
44 43 simprbi 
 |-  ( ( z D y ) e. ( 0 [,] +oo ) -> 0 <_ ( z D y ) )
45 40 44 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> 0 <_ ( z D y ) )
46 ge0nemnf 
 |-  ( ( ( z D y ) e. RR* /\ 0 <_ ( z D y ) ) -> ( z D y ) =/= -oo )
47 42 45 46 syl2anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) =/= -oo )
48 47 a1d 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( -. ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) -> ( z D y ) =/= -oo ) )
49 48 necon4bd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z D y ) = -oo -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
50 49 adantr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( ( z D y ) = -oo -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
51 50 imp 
 |-  ( ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) /\ ( z D y ) = -oo ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
52 42 adantr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( z D y ) e. RR* )
53 elxr 
 |-  ( ( z D y ) e. RR* <-> ( ( z D y ) e. RR \/ ( z D y ) = +oo \/ ( z D y ) = -oo ) )
54 52 53 sylib 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( ( z D y ) e. RR \/ ( z D y ) = +oo \/ ( z D y ) = -oo ) )
55 16 38 51 54 mpjao3dan 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
56 19 adantr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( x D y ) <_ +oo )
57 oveq1 
 |-  ( ( z D x ) = +oo -> ( ( z D x ) +e ( z D y ) ) = ( +oo +e ( z D y ) ) )
58 xaddpnf2 
 |-  ( ( ( z D y ) e. RR* /\ ( z D y ) =/= -oo ) -> ( +oo +e ( z D y ) ) = +oo )
59 42 47 58 syl2anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( +oo +e ( z D y ) ) = +oo )
60 57 59 sylan9eqr 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( ( z D x ) +e ( z D y ) ) = +oo )
61 56 60 breqtrrd 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
62 elxrge0 
 |-  ( ( z D x ) e. ( 0 [,] +oo ) <-> ( ( z D x ) e. RR* /\ 0 <_ ( z D x ) ) )
63 62 simprbi 
 |-  ( ( z D x ) e. ( 0 [,] +oo ) -> 0 <_ ( z D x ) )
64 31 63 syl 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> 0 <_ ( z D x ) )
65 ge0nemnf 
 |-  ( ( ( z D x ) e. RR* /\ 0 <_ ( z D x ) ) -> ( z D x ) =/= -oo )
66 33 64 65 syl2anc 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) =/= -oo )
67 66 a1d 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( -. ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) -> ( z D x ) =/= -oo ) )
68 67 necon4bd 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z D x ) = -oo -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
69 68 imp 
 |-  ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = -oo ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
70 elxr 
 |-  ( ( z D x ) e. RR* <-> ( ( z D x ) e. RR \/ ( z D x ) = +oo \/ ( z D x ) = -oo ) )
71 33 70 sylib 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z D x ) e. RR \/ ( z D x ) = +oo \/ ( z D x ) = -oo ) )
72 55 61 69 71 mpjao3dan 
 |-  ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
73 1 2 11 72 isxmetd 
 |-  ( ph -> D e. ( *Met ` X ) )