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

Theorem isxmet2d 17892
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.)
Hypotheses
Ref Expression
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
Ref Expression
isxmet2d  |-  ( ph  ->  D  e.  ( * Met `  X ) )
Distinct variable groups:    x, y,
z, D    ph, x, y, z    x, X, y, z

Proof of Theorem isxmet2d
StepHypRef Expression
1 isxmetd.0 . 2  |-  ( ph  ->  X  e.  _V )
2 isxmetd.1 . 2  |-  ( ph  ->  D : ( X  X.  X ) --> RR* )
3 fovrn 5990 . . . . . 6  |-  ( ( D : ( X  X.  X ) --> RR* 
/\  x  e.  X  /\  y  e.  X
)  ->  ( x D y )  e. 
RR* )
433expb 1152 . . . . 5  |-  ( ( D : ( X  X.  X ) --> RR* 
/\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x D y )  e.  RR* )
52, 4sylan 457 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x D y )  e.  RR* )
6 0xr 8878 . . . 4  |-  0  e.  RR*
7 xrletri3 10486 . . . 4  |-  ( ( ( x D y )  e.  RR*  /\  0  e.  RR* )  ->  (
( x D y )  =  0  <->  (
( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
85, 6, 7sylancl 643 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  =  0  <-> 
( ( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
9 isxmet2d.2 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
0  <_  ( x D y ) )
109biantrud 493 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  <_  0  <->  ( ( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
11 isxmet2d.3 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  <_  0  <->  x  =  y ) )
128, 10, 113bitr2d 272 . 2  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  =  0  <-> 
x  =  y ) )
13 ffn 5389 . . . . . . . . 9  |-  ( D : ( X  X.  X ) --> RR*  ->  D  Fn  ( X  X.  X ) )
142, 13syl 15 . . . . . . . 8  |-  ( ph  ->  D  Fn  ( X  X.  X ) )
15 elxrge0 10747 . . . . . . . . . 10  |-  ( ( x D y )  e.  ( 0 [,] 
+oo )  <->  ( (
x D y )  e.  RR*  /\  0  <_  ( x D y ) ) )
165, 9, 15sylanbrc 645 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x D y )  e.  ( 0 [,]  +oo ) )
1716ralrimivva 2635 . . . . . . . 8  |-  ( ph  ->  A. x  e.  X  A. y  e.  X  ( x D y )  e.  ( 0 [,]  +oo ) )
18 ffnov 5948 . . . . . . . 8  |-  ( 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 ) ) )
1914, 17, 18sylanbrc 645 . . . . . . 7  |-  ( ph  ->  D : ( X  X.  X ) --> ( 0 [,]  +oo )
)
2019adantr 451 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  ->  D : ( X  X.  X ) --> ( 0 [,]  +oo ) )
21 simpr3 963 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
z  e.  X )
22 simpr1 961 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  ->  x  e.  X )
23 fovrn 5990 . . . . . 6  |-  ( ( D : ( X  X.  X ) --> ( 0 [,]  +oo )  /\  z  e.  X  /\  x  e.  X
)  ->  ( z D x )  e.  ( 0 [,]  +oo ) )
2420, 21, 22, 23syl3anc 1182 . . . . 5  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  e.  ( 0 [,]  +oo ) )
25 elxrge0 10747 . . . . . 6  |-  ( ( z D x )  e.  ( 0 [,] 
+oo )  <->  ( (
z D x )  e.  RR*  /\  0  <_  ( z D x ) ) )
2625simplbi 446 . . . . 5  |-  ( ( z D x )  e.  ( 0 [,] 
+oo )  ->  (
z D x )  e.  RR* )
2724, 26syl 15 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  e.  RR* )
28 elxr 10458 . . . 4  |-  ( ( z D x )  e.  RR*  <->  ( ( z D x )  e.  RR  \/  ( z D x )  = 
+oo  \/  ( z D x )  = 
-oo ) )
2927, 28sylib 188 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( ( z D x )  e.  RR  \/  ( z D x )  =  +oo  \/  ( z D x )  =  -oo )
)
30 simpr2 962 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
y  e.  X )
31 fovrn 5990 . . . . . . . . 9  |-  ( ( D : ( X  X.  X ) --> ( 0 [,]  +oo )  /\  z  e.  X  /\  y  e.  X
)  ->  ( z D y )  e.  ( 0 [,]  +oo ) )
3220, 21, 30, 31syl3anc 1182 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  e.  ( 0 [,]  +oo ) )
33 elxrge0 10747 . . . . . . . . 9  |-  ( ( z D y )  e.  ( 0 [,] 
+oo )  <->  ( (
z D y )  e.  RR*  /\  0  <_  ( z D y ) ) )
3433simplbi 446 . . . . . . . 8  |-  ( ( z D y )  e.  ( 0 [,] 
+oo )  ->  (
z D y )  e.  RR* )
3532, 34syl 15 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  e.  RR* )
3635adantr 451 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  e.  RR )  ->  (
z D y )  e.  RR* )
37 elxr 10458 . . . . . 6  |-  ( ( z D y )  e.  RR*  <->  ( ( z D y )  e.  RR  \/  ( z D y )  = 
+oo  \/  ( z D y )  = 
-oo ) )
3836, 37sylib 188 . . . . 5  |-  ( ( ( 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 )
)
39 isxmet2d.4 . . . . . . . . 9  |-  ( (
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 ) ) )
40393expa 1151 . . . . . . . 8  |-  ( ( ( 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 ) ) )
41 rexadd 10559 . . . . . . . . 9  |-  ( ( ( z D x )  e.  RR  /\  ( z D y )  e.  RR )  ->  ( ( z D x ) + e ( z D y ) )  =  ( ( z D x )  +  ( z D y ) ) )
4241adantl 452 . . . . . . . 8  |-  ( ( ( 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 ) ) )
4340, 42breqtrrd 4049 . . . . . . 7  |-  ( ( ( 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 ) ) )
4443anassrs 629 . . . . . 6  |-  ( ( ( ( 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 ) ) )
4553adantr3 1116 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  e.  RR* )
46 pnfge 10469 . . . . . . . . 9  |-  ( ( x D y )  e.  RR*  ->  ( x D y )  <_  +oo )
4745, 46syl 15 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  <_  +oo )
4847ad2antrr 706 . . . . . . 7  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X
) )  /\  (
z D x )  e.  RR )  /\  ( z D y )  =  +oo )  ->  ( x D y )  <_  +oo )
49 oveq2 5866 . . . . . . . 8  |-  ( ( z D y )  =  +oo  ->  (
( z D x ) + e ( z D y ) )  =  ( ( z D x ) + e  +oo )
)
50 renemnf 8880 . . . . . . . . 9  |-  ( ( z D x )  e.  RR  ->  (
z D x )  =/=  -oo )
51 xaddpnf1 10553 . . . . . . . . 9  |-  ( ( ( z D x )  e.  RR*  /\  (
z D x )  =/=  -oo )  ->  (
( z D x ) + e  +oo )  =  +oo )
5227, 50, 51syl2an 463 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  e.  RR )  ->  (
( z D x ) + e  +oo )  =  +oo )
5349, 52sylan9eqr 2337 . . . . . . 7  |-  ( ( ( ( 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 )
5448, 53breqtrrd 4049 . . . . . 6  |-  ( ( ( ( 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 ) ) )
5533simprbi 450 . . . . . . . . . . . 12  |-  ( ( z D y )  e.  ( 0 [,] 
+oo )  ->  0  <_  ( z D y ) )
5632, 55syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
0  <_  ( z D y ) )
57 ge0nemnf 10502 . . . . . . . . . . 11  |-  ( ( ( z D y )  e.  RR*  /\  0  <_  ( z D y ) )  ->  (
z D y )  =/=  -oo )
5835, 56, 57syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  =/=  -oo )
5958a1d 22 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( -.  ( x D y )  <_ 
( ( z D x ) + e
( z D y ) )  ->  (
z D y )  =/=  -oo ) )
6059necon4bd 2508 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( ( z D y )  =  -oo  ->  ( x D y )  <_  ( (
z D x ) + e ( z D y ) ) ) )
6160adantr 451 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
6261imp 418 . . . . . 6  |-  ( ( ( ( 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 ) ) )
6344, 54, 623jaodan 1248 . . . . 5  |-  ( ( ( ( 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 )
)  ->  ( x D y )  <_ 
( ( z D x ) + e
( z D y ) ) )
6438, 63mpdan 649 . . . 4  |-  ( ( ( 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 ) ) )
6547adantr 451 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = 
+oo )  ->  (
x D y )  <_  +oo )
66 oveq1 5865 . . . . . 6  |-  ( ( z D x )  =  +oo  ->  (
( z D x ) + e ( z D y ) )  =  (  +oo + e ( z D y ) ) )
67 xaddpnf2 10554 . . . . . . 7  |-  ( ( ( z D y )  e.  RR*  /\  (
z D y )  =/=  -oo )  ->  (  +oo + e ( z D y ) )  =  +oo )
6835, 58, 67syl2anc 642 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
(  +oo + e ( z D y ) )  =  +oo )
6966, 68sylan9eqr 2337 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = 
+oo )  ->  (
( z D x ) + e ( z D y ) )  =  +oo )
7065, 69breqtrrd 4049 . . . 4  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = 
+oo )  ->  (
x D y )  <_  ( ( z D x ) + e ( z D y ) ) )
7125simprbi 450 . . . . . . . . 9  |-  ( ( z D x )  e.  ( 0 [,] 
+oo )  ->  0  <_  ( z D x ) )
7224, 71syl 15 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
0  <_  ( z D x ) )
73 ge0nemnf 10502 . . . . . . . 8  |-  ( ( ( z D x )  e.  RR*  /\  0  <_  ( z D x ) )  ->  (
z D x )  =/=  -oo )
7427, 72, 73syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  =/=  -oo )
7574a1d 22 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( -.  ( x D y )  <_ 
( ( z D x ) + e
( z D y ) )  ->  (
z D x )  =/=  -oo ) )
7675necon4bd 2508 . . . . 5  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( ( z D x )  =  -oo  ->  ( x D y )  <_  ( (
z D x ) + e ( z D y ) ) ) )
7776imp 418 . . . 4  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = 
-oo )  ->  (
x D y )  <_  ( ( z D x ) + e ( z D y ) ) )
7864, 70, 773jaodan 1248 . . 3  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( (
z D x )  e.  RR  \/  (
z D x )  =  +oo  \/  (
z D x )  =  -oo ) )  ->  ( x D y )  <_  (
( z D x ) + e ( z D y ) ) )
7929, 78mpdan 649 . 2  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  <_  ( (
z D x ) + e ( z D y ) ) )
801, 2, 12, 79isxmetd 17891 1  |-  ( ph  ->  D  e.  ( * Met `  X ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    \/ w3o 933    /\ w3a 934    = wceq 1623    e. wcel 1684    =/= wne 2446   A.wral 2543   _Vcvv 2788   class class class wbr 4023    X. cxp 4687    Fn wfn 5250   -->wf 5251   ` cfv 5255  (class class class)co 5858   RRcr 8736   0cc0 8737    + caddc 8740    +oocpnf 8864    -oocmnf 8865   RR*cxr 8866    <_ cle 8868   + ecxad 10450   [,]cicc 10659   * Metcxmt 16369
This theorem is referenced by:  prdsxmetlem  17932  xrsxmet  18315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-po 4314  df-so 4315  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-er 6660  df-map 6774  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-xadd 10453  df-icc 10663  df-xmet 16373
  Copyright terms: Public domain W3C validator