Theorem isxmet2d 13515

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

Step	Hyp	Ref	Expression
1		isxmetd.0	. 2 |- ( ph -> X e. _V )
2		isxmetd.1	. 2 |- ( ph -> D : ( X X. X ) --> RR* )
3	2	fovcdmda 6012	. . . 4 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) e. RR* )
4		0xr 7994	. . . 4 |- 0 e. RR*
5		xrletri3 9791	. . . 4 |- ( ( ( x D y ) e. RR* /\ 0 e. RR* ) -> ( ( x D y ) = 0 <-> ( ( x D y ) <_ 0 /\ 0 <_ ( x D y ) ) ) )
6	3, 4, 5	sylancl 413	. . 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 ) )
8	7	biantrud 304	. . 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 ) )
10	6, 8, 9	3bitr2d 216	. 2 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )
11		isxmet2d.4	. . . . . . 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 ) + ( z D y ) ) )
12	11	3expa 1203	. . . . . 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 ) + ( z D y ) ) )
13		rexadd 9839	. . . . . . 7 |- ( ( ( 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 277	. . . . . 6 |- ( ( ( 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 4028	. . . . 5 |- ( ( ( 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 400	. . . 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 ) +e ( z D y ) ) )
17	3	3adantr3 1158	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) e. RR* )
18		pnfge 9776	. . . . . . 7 |- ( ( x D y ) e. RR* -> ( x D y ) <_ +oo )
19	17, 18	syl 14	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ +oo )
20	19	ad2antrr 488	. . . . 5 |- ( ( ( ( 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 5877	. . . . . 6 |- ( ( z D y ) = +oo -> ( ( z D x ) +e ( z D y ) ) = ( ( z D x ) +e +oo ) )
22	2	ffnd 5362	. . . . . . . . . . 11 |- ( ph -> D Fn ( X X. X ) )
23		elxrge0 9965	. . . . . . . . . . . . 13 |- ( ( x D y ) e. ( 0 [,] +oo ) <-> ( ( x D y ) e. RR* /\ 0 <_ ( x D y ) ) )
24	3, 7, 23	sylanbrc 417	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( x D y ) e. ( 0 [,] +oo ) )
25	24	ralrimivva 2559	. . . . . . . . . . 11 |- ( ph -> A. x e. X A. y e. X ( x D y ) e. ( 0 [,] +oo ) )
26		ffnov 5973	. . . . . . . . . . 11 |- ( 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 417	. . . . . . . . . 10 |- ( ph -> D : ( X X. X ) --> ( 0 [,] +oo ) )
28	27	adantr 276	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )
29		simpr3 1005	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> z e. X )
30		simpr1 1003	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> x e. X )
31	28, 29, 30	fovcdmd 6013	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) e. ( 0 [,] +oo ) )
32		elxrge0 9965	. . . . . . . . 9 |- ( ( z D x ) e. ( 0 [,] +oo ) <-> ( ( z D x ) e. RR* /\ 0 <_ ( z D x ) ) )
33	32	simplbi 274	. . . . . . . 8 |- ( ( z D x ) e. ( 0 [,] +oo ) -> ( z D x ) e. RR* )
34	31, 33	syl 14	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) e. RR* )
35		renemnf 7996	. . . . . . 7 |- ( ( z D x ) e. RR -> ( z D x ) =/= -oo )
36		xaddpnf1 9833	. . . . . . 7 |- ( ( ( z D x ) e. RR* /\ ( z D x ) =/= -oo ) -> ( ( z D x ) +e +oo ) = +oo )
37	34, 35, 36	syl2an 289	. . . . . 6 |- ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( ( z D x ) +e +oo ) = +oo )
38	21, 37	sylan9eqr 2232	. . . . 5 |- ( ( ( ( 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 )
39	20, 38	breqtrrd 4028	. . . 4 |- ( ( ( ( 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 ) ) )
40		simpr2 1004	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> y e. X )
41	28, 29, 40	fovcdmd 6013	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) e. ( 0 [,] +oo ) )
42		elxrge0 9965	. . . . . . . . . . 11 |- ( ( z D y ) e. ( 0 [,] +oo ) <-> ( ( z D y ) e. RR* /\ 0 <_ ( z D y ) ) )
43	42	simplbi 274	. . . . . . . . . 10 |- ( ( z D y ) e. ( 0 [,] +oo ) -> ( z D y ) e. RR* )
44	41, 43	syl 14	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) e. RR* )
45	42	simprbi 275	. . . . . . . . . 10 |- ( ( z D y ) e. ( 0 [,] +oo ) -> 0 <_ ( z D y ) )
46	41, 45	syl 14	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> 0 <_ ( z D y ) )
47		ge0nemnf 9811	. . . . . . . . 9 |- ( ( ( z D y ) e. RR* /\ 0 <_ ( z D y ) ) -> ( z D y ) =/= -oo )
48	44, 46, 47	syl2anc 411	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D y ) =/= -oo )
49	48	neneqd 2368	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> -. ( z D y ) = -oo )
50	49	pm2.21d 619	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z D y ) = -oo -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) )
51	50	adantr 276	. . . . 5 |- ( ( ( 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	51	imp 124	. . . 4 |- ( ( ( ( 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 ) ) )
53	44	adantr 276	. . . . 5 |- ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) e. RR ) -> ( z D y ) e. RR* )
54		elxr 9763	. . . . 5 |- ( ( z D y ) e. RR* <-> ( ( z D y ) e. RR \/ ( z D y ) = +oo \/ ( z D y ) = -oo ) )
55	53, 54	sylib 122	. . . 4 |- ( ( ( 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 ) )
56	16, 39, 52, 55	mpjao3dan 1307	. . 3 |- ( ( ( 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 ) ) )
57	19	adantr 276	. . . 4 |- ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( x D y ) <_ +oo )
58		oveq1 5876	. . . . 5 |- ( ( z D x ) = +oo -> ( ( z D x ) +e ( z D y ) ) = ( +oo +e ( z D y ) ) )
59		xaddpnf2 9834	. . . . . 6 |- ( ( ( z D y ) e. RR* /\ ( z D y ) =/= -oo ) -> ( +oo +e ( z D y ) ) = +oo )
60	44, 48, 59	syl2anc 411	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( +oo +e ( z D y ) ) = +oo )
61	58, 60	sylan9eqr 2232	. . . 4 |- ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( ( z D x ) +e ( z D y ) ) = +oo )
62	57, 61	breqtrrd 4028	. . 3 |- ( ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) /\ ( z D x ) = +oo ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
63	32	simprbi 275	. . . . . . . 8 |- ( ( z D x ) e. ( 0 [,] +oo ) -> 0 <_ ( z D x ) )
64	31, 63	syl 14	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> 0 <_ ( z D x ) )
65		ge0nemnf 9811	. . . . . . 7 |- ( ( ( z D x ) e. RR* /\ 0 <_ ( z D x ) ) -> ( z D x ) =/= -oo )
66	34, 64, 65	syl2anc 411	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( z D x ) =/= -oo )
67	66	neneqd 2368	. . . . 5 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> -. ( z D x ) = -oo )
68	67	pm2.21d 619	. . . 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 ) ) ) )
69	68	imp 124	. . 3 |- ( ( ( 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 9763	. . . 4 |- ( ( z D x ) e. RR* <-> ( ( z D x ) e. RR \/ ( z D x ) = +oo \/ ( z D x ) = -oo ) )
71	34, 70	sylib 122	. . 3 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( z D x ) e. RR \/ ( z D x ) = +oo \/ ( z D x ) = -oo ) )
72	56, 62, 69, 71	mpjao3dan 1307	. 2 |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )
73	1, 2, 10, 72	isxmetd 13514	1 |- ( ph -> D e. ( *Met ` X ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   \/ w3o 977   /\ w3a 978   = wceq 1353   e. wcel 2148   =/= wne 2347   A.wral 2455   _Vcvv 2737   class class class wbr 4000   X. cxp 4621   Fn wfn 5207   -->wf 5208   ` cfv 5212  (class class class)co 5869   RRcr 7801   0cc0 7802   + caddc 7805   +oocpnf 7979   -oocmnf 7980   RR*cxr 7981   <_ cle 7983   +ecxad 9757   [,]cicc 9878   *Metcxmet 13147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7893  ax-resscn 7894  ax-1re 7896  ax-addrcl 7899  ax-rnegex 7911  ax-pre-ltirr 7914  ax-pre-ltwlin 7915  ax-pre-lttrn 7916  ax-pre-apti 7917

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-po 4293  df-iso 4294  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-map 6644  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-xadd 9760  df-icc 9882  df-xmet 13155

This theorem is referenced by: (None)