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

Theorem isxmet2d 20560
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* )
32fovrnda 6423 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x D y )  e.  RR* )
4 0xr 9631 . . . 4  |-  0  e.  RR*
5 xrletri3 11349 . . . 4  |-  ( ( ( x D y )  e.  RR*  /\  0  e.  RR* )  ->  (
( x D y )  =  0  <->  (
( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
63, 4, 5sylancl 662 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  =  0  <-> 
( ( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
7 isxmet2d.2 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
0  <_  ( x D y ) )
87biantrud 507 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  <_  0  <->  ( ( x D y )  <_  0  /\  0  <_  ( x D y ) ) ) )
9 isxmet2d.3 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  <_  0  <->  x  =  y ) )
106, 8, 93bitr2d 281 . 2  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( x D y )  =  0  <-> 
x  =  y ) )
11 ffn 5724 . . . . . . . . 9  |-  ( D : ( X  X.  X ) --> RR*  ->  D  Fn  ( X  X.  X ) )
122, 11syl 16 . . . . . . . 8  |-  ( ph  ->  D  Fn  ( X  X.  X ) )
13 elxrge0 11620 . . . . . . . . . 10  |-  ( ( x D y )  e.  ( 0 [,] +oo )  <->  ( ( x D y )  e. 
RR*  /\  0  <_  ( x D y ) ) )
143, 7, 13sylanbrc 664 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x D y )  e.  ( 0 [,] +oo ) )
1514ralrimivva 2880 . . . . . . . 8  |-  ( ph  ->  A. x  e.  X  A. y  e.  X  ( x D y )  e.  ( 0 [,] +oo ) )
16 ffnov 6383 . . . . . . . 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 ) ) )
1712, 15, 16sylanbrc 664 . . . . . . 7  |-  ( ph  ->  D : ( X  X.  X ) --> ( 0 [,] +oo )
)
1817adantr 465 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  ->  D : ( X  X.  X ) --> ( 0 [,] +oo ) )
19 simpr3 999 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
z  e.  X )
20 simpr1 997 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  ->  x  e.  X )
2118, 19, 20fovrnd 6424 . . . . 5  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  e.  ( 0 [,] +oo ) )
22 elxrge0 11620 . . . . . 6  |-  ( ( z D x )  e.  ( 0 [,] +oo )  <->  ( ( z D x )  e. 
RR*  /\  0  <_  ( z D x ) ) )
2322simplbi 460 . . . . 5  |-  ( ( z D x )  e.  ( 0 [,] +oo )  ->  ( z D x )  e. 
RR* )
2421, 23syl 16 . . . 4  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  e.  RR* )
25 elxr 11316 . . . 4  |-  ( ( z D x )  e.  RR*  <->  ( ( z D x )  e.  RR  \/  ( z D x )  = +oo  \/  ( z D x )  = -oo ) )
2624, 25sylib 196 . . 3  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( ( z D x )  e.  RR  \/  ( z D x )  = +oo  \/  ( z D x )  = -oo )
)
27 simpr2 998 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
y  e.  X )
2818, 19, 27fovrnd 6424 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  e.  ( 0 [,] +oo ) )
29 elxrge0 11620 . . . . . . . . 9  |-  ( ( z D y )  e.  ( 0 [,] +oo )  <->  ( ( z D y )  e. 
RR*  /\  0  <_  ( z D y ) ) )
3029simplbi 460 . . . . . . . 8  |-  ( ( z D y )  e.  ( 0 [,] +oo )  ->  ( z D y )  e. 
RR* )
3128, 30syl 16 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  e.  RR* )
3231adantr 465 . . . . . 6  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  e.  RR )  ->  (
z D y )  e.  RR* )
33 elxr 11316 . . . . . 6  |-  ( ( z D y )  e.  RR*  <->  ( ( z D y )  e.  RR  \/  ( z D y )  = +oo  \/  ( z D y )  = -oo ) )
3432, 33sylib 196 . . . . 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 )
)
35 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 ) ) )
36353expa 1191 . . . . . . . 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 ) ) )
37 rexadd 11422 . . . . . . . . 9  |-  ( ( ( z D x )  e.  RR  /\  ( z D y )  e.  RR )  ->  ( ( z D x ) +e ( z D y ) )  =  ( ( z D x )  +  ( z D y ) ) )
3837adantl 466 . . . . . . . 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 ) ) )
3936, 38breqtrrd 4468 . . . . . . 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 ) ) )
4039anassrs 648 . . . . . 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 ) ) )
4133adantr3 1152 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  e.  RR* )
42 pnfge 11330 . . . . . . . . 9  |-  ( ( x D y )  e.  RR*  ->  ( x D y )  <_ +oo )
4341, 42syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  <_ +oo )
4443ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X
) )  /\  (
z D x )  e.  RR )  /\  ( z D y )  = +oo )  ->  ( x D y )  <_ +oo )
45 oveq2 6285 . . . . . . . 8  |-  ( ( z D y )  = +oo  ->  (
( z D x ) +e ( z D y ) )  =  ( ( z D x ) +e +oo )
)
46 renemnf 9633 . . . . . . . . 9  |-  ( ( z D x )  e.  RR  ->  (
z D x )  =/= -oo )
47 xaddpnf1 11416 . . . . . . . . 9  |-  ( ( ( z D x )  e.  RR*  /\  (
z D x )  =/= -oo )  -> 
( ( z D x ) +e +oo )  = +oo )
4824, 46, 47syl2an 477 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  e.  RR )  ->  (
( z D x ) +e +oo )  = +oo )
4945, 48sylan9eqr 2525 . . . . . . 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 )
5044, 49breqtrrd 4468 . . . . . 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 ) ) )
5129simprbi 464 . . . . . . . . . . . 12  |-  ( ( z D y )  e.  ( 0 [,] +oo )  ->  0  <_ 
( z D y ) )
5228, 51syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
0  <_  ( z D y ) )
53 ge0nemnf 11365 . . . . . . . . . . 11  |-  ( ( ( z D y )  e.  RR*  /\  0  <_  ( z D y ) )  ->  (
z D y )  =/= -oo )
5431, 52, 53syl2anc 661 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D y )  =/= -oo )
5554a1d 25 . . . . . . . . 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 ) )
5655necon4bd 2684 . . . . . . . 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 ) ) ) )
5756adantr 465 . . . . . . 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 ) ) ) )
5857imp 429 . . . . . 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 ) ) )
5940, 50, 583jaodan 1289 . . . . 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 ) ) )
6034, 59mpdan 668 . . . 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 ) ) )
6143adantr 465 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = +oo )  ->  (
x D y )  <_ +oo )
62 oveq1 6284 . . . . . 6  |-  ( ( z D x )  = +oo  ->  (
( z D x ) +e ( z D y ) )  =  ( +oo +e ( z D y ) ) )
63 xaddpnf2 11417 . . . . . . 7  |-  ( ( ( z D y )  e.  RR*  /\  (
z D y )  =/= -oo )  -> 
( +oo +e ( z D y ) )  = +oo )
6431, 54, 63syl2anc 661 . . . . . 6  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( +oo +e ( z D y ) )  = +oo )
6562, 64sylan9eqr 2525 . . . . 5  |-  ( ( ( ph  /\  (
x  e.  X  /\  y  e.  X  /\  z  e.  X )
)  /\  ( z D x )  = +oo )  ->  (
( z D x ) +e ( z D y ) )  = +oo )
6661, 65breqtrrd 4468 . . . 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 ) ) )
6722simprbi 464 . . . . . . . . 9  |-  ( ( z D x )  e.  ( 0 [,] +oo )  ->  0  <_ 
( z D x ) )
6821, 67syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
0  <_  ( z D x ) )
69 ge0nemnf 11365 . . . . . . . 8  |-  ( ( ( z D x )  e.  RR*  /\  0  <_  ( z D x ) )  ->  (
z D x )  =/= -oo )
7024, 68, 69syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( z D x )  =/= -oo )
7170a1d 25 . . . . . 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 ) )
7271necon4bd 2684 . . . . 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 ) ) ) )
7372imp 429 . . . 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 ) ) )
7460, 66, 733jaodan 1289 . . 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 ) ) )
7526, 74mpdan 668 . 2  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X  /\  z  e.  X ) )  -> 
( x D y )  <_  ( (
z D x ) +e ( z D y ) ) )
761, 2, 10, 75isxmetd 20559 1  |-  ( ph  ->  D  e.  ( *Met `  X ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    \/ w3o 967    /\ w3a 968    = wceq 1374    e. wcel 1762    =/= wne 2657   A.wral 2809   _Vcvv 3108   class class class wbr 4442    X. cxp 4992    Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6277   RRcr 9482   0cc0 9483    + caddc 9486   +oocpnf 9616   -oocmnf 9617   RR*cxr 9618    <_ cle 9620   +ecxad 11307   [,]cicc 11523   *Metcxmt 18169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-i2m1 9551  ax-1ne0 9552  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-op 4029  df-uni 4241  df-iun 4322  df-br 4443  df-opab 4501  df-mpt 4502  df-id 4790  df-po 4795  df-so 4796  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-er 7303  df-map 7414  df-en 7509  df-dom 7510  df-sdom 7511  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-xadd 11310  df-icc 11527  df-xmet 18178
This theorem is referenced by:  prdsxmetlem  20601  xrsxmet  21044
  Copyright terms: Public domain W3C validator