Metamath Proof Explorer


Theorem metdstri

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ) . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis metdscn.f F=xXsupranySxDy*<
Assertion metdstri D∞MetXSXAXBXFAADB+𝑒FB

Proof

Step Hyp Ref Expression
1 metdscn.f F=xXsupranySxDy*<
2 simprr D∞MetXSXAXBXADBFAFA
3 simprl D∞MetXSXAXBXADBFAADB
4 rexsub FAADBFA+𝑒ADB=FAADB
5 2 3 4 syl2anc D∞MetXSXAXBXADBFAFA+𝑒ADB=FAADB
6 5 oveq2d D∞MetXSXAXBXADBFABballDFA+𝑒ADB=BballDFAADB
7 simpll D∞MetXSXAXBXD∞MetX
8 7 adantr D∞MetXSXAXBXADBFAD∞MetX
9 simprr D∞MetXSXAXBXBX
10 9 adantr D∞MetXSXAXBXADBFABX
11 simprl D∞MetXSXAXBXAX
12 11 adantr D∞MetXSXAXBXADBFAAX
13 2 3 resubcld D∞MetXSXAXBXADBFAFAADB
14 3 leidd D∞MetXSXAXBXADBFAADBADB
15 xmetsym D∞MetXAXBXADB=BDA
16 7 11 9 15 syl3anc D∞MetXSXAXBXADB=BDA
17 16 adantr D∞MetXSXAXBXADBFAADB=BDA
18 17 eqcomd D∞MetXSXAXBXADBFABDA=ADB
19 2 recnd D∞MetXSXAXBXADBFAFA
20 3 recnd D∞MetXSXAXBXADBFAADB
21 19 20 nncand D∞MetXSXAXBXADBFAFAFAADB=ADB
22 14 18 21 3brtr4d D∞MetXSXAXBXADBFABDAFAFAADB
23 blss2 D∞MetXBXAXFAADBFABDAFAFAADBBballDFAADBAballDFA
24 8 10 12 13 2 22 23 syl33anc D∞MetXSXAXBXADBFABballDFAADBAballDFA
25 6 24 eqsstrd D∞MetXSXAXBXADBFABballDFA+𝑒ADBAballDFA
26 25 expr D∞MetXSXAXBXADBFABballDFA+𝑒ADBAballDFA
27 7 adantr D∞MetXSXAXBXADBFA=+∞D∞MetX
28 9 adantr D∞MetXSXAXBXADBFA=+∞BX
29 1 metdsf D∞MetXSXF:X0+∞
30 29 adantr D∞MetXSXAXBXF:X0+∞
31 30 11 ffvelrnd D∞MetXSXAXBXFA0+∞
32 eliccxr FA0+∞FA*
33 31 32 syl D∞MetXSXAXBXFA*
34 33 adantr D∞MetXSXAXBXADBFA*
35 xmetcl D∞MetXAXBXADB*
36 7 11 9 35 syl3anc D∞MetXSXAXBXADB*
37 36 adantr D∞MetXSXAXBXADBADB*
38 37 xnegcld D∞MetXSXAXBXADBADB*
39 34 38 xaddcld D∞MetXSXAXBXADBFA+𝑒ADB*
40 39 adantrr D∞MetXSXAXBXADBFA=+∞FA+𝑒ADB*
41 pnfxr +∞*
42 41 a1i D∞MetXSXAXBXADBFA=+∞+∞*
43 pnfge FA+𝑒ADB*FA+𝑒ADB+∞
44 40 43 syl D∞MetXSXAXBXADBFA=+∞FA+𝑒ADB+∞
45 ssbl D∞MetXBXFA+𝑒ADB*+∞*FA+𝑒ADB+∞BballDFA+𝑒ADBBballD+∞
46 27 28 40 42 44 45 syl221anc D∞MetXSXAXBXADBFA=+∞BballDFA+𝑒ADBBballD+∞
47 simprr D∞MetXSXAXBXADBFA=+∞FA=+∞
48 47 oveq2d D∞MetXSXAXBXADBFA=+∞AballDFA=AballD+∞
49 11 adantr D∞MetXSXAXBXADBFA=+∞AX
50 simprl D∞MetXSXAXBXADBFA=+∞ADB
51 xblpnf D∞MetXAXBAballD+∞BXADB
52 27 49 51 syl2anc D∞MetXSXAXBXADBFA=+∞BAballD+∞BXADB
53 28 50 52 mpbir2and D∞MetXSXAXBXADBFA=+∞BAballD+∞
54 blpnfctr D∞MetXAXBAballD+∞AballD+∞=BballD+∞
55 27 49 53 54 syl3anc D∞MetXSXAXBXADBFA=+∞AballD+∞=BballD+∞
56 48 55 eqtr2d D∞MetXSXAXBXADBFA=+∞BballD+∞=AballDFA
57 46 56 sseqtrd D∞MetXSXAXBXADBFA=+∞BballDFA+𝑒ADBAballDFA
58 57 expr D∞MetXSXAXBXADBFA=+∞BballDFA+𝑒ADBAballDFA
59 elxrge0 FA0+∞FA*0FA
60 59 simprbi FA0+∞0FA
61 31 60 syl D∞MetXSXAXBX0FA
62 ge0nemnf FA*0FAFA−∞
63 33 61 62 syl2anc D∞MetXSXAXBXFA−∞
64 33 63 jca D∞MetXSXAXBXFA*FA−∞
65 64 adantr D∞MetXSXAXBXADBFA*FA−∞
66 xrnemnf FA*FA−∞FAFA=+∞
67 65 66 sylib D∞MetXSXAXBXADBFAFA=+∞
68 26 58 67 mpjaod D∞MetXSXAXBXADBBballDFA+𝑒ADBAballDFA
69 pnfnlt FA*¬+∞<FA
70 33 69 syl D∞MetXSXAXBX¬+∞<FA
71 70 adantr D∞MetXSXAXBXADB=+∞¬+∞<FA
72 36 xnegcld D∞MetXSXAXBXADB*
73 33 72 xaddcld D∞MetXSXAXBXFA+𝑒ADB*
74 xbln0 D∞MetXBXFA+𝑒ADB*BballDFA+𝑒ADB0<FA+𝑒ADB
75 7 9 73 74 syl3anc D∞MetXSXAXBXBballDFA+𝑒ADB0<FA+𝑒ADB
76 xposdif ADB*FA*ADB<FA0<FA+𝑒ADB
77 36 33 76 syl2anc D∞MetXSXAXBXADB<FA0<FA+𝑒ADB
78 75 77 bitr4d D∞MetXSXAXBXBballDFA+𝑒ADBADB<FA
79 breq1 ADB=+∞ADB<FA+∞<FA
80 78 79 sylan9bb D∞MetXSXAXBXADB=+∞BballDFA+𝑒ADB+∞<FA
81 80 necon1bbid D∞MetXSXAXBXADB=+∞¬+∞<FABballDFA+𝑒ADB=
82 71 81 mpbid D∞MetXSXAXBXADB=+∞BballDFA+𝑒ADB=
83 0ss AballDFA
84 82 83 eqsstrdi D∞MetXSXAXBXADB=+∞BballDFA+𝑒ADBAballDFA
85 xmetge0 D∞MetXAXBX0ADB
86 7 11 9 85 syl3anc D∞MetXSXAXBX0ADB
87 ge0nemnf ADB*0ADBADB−∞
88 36 86 87 syl2anc D∞MetXSXAXBXADB−∞
89 36 88 jca D∞MetXSXAXBXADB*ADB−∞
90 xrnemnf ADB*ADB−∞ADBADB=+∞
91 89 90 sylib D∞MetXSXAXBXADBADB=+∞
92 68 84 91 mpjaodan D∞MetXSXAXBXBballDFA+𝑒ADBAballDFA
93 sslin BballDFA+𝑒ADBAballDFASBballDFA+𝑒ADBSAballDFA
94 92 93 syl D∞MetXSXAXBXSBballDFA+𝑒ADBSAballDFA
95 33 xrleidd D∞MetXSXAXBXFAFA
96 simplr D∞MetXSXAXBXSX
97 1 metdsge D∞MetXSXAXFA*FAFASAballDFA=
98 7 96 11 33 97 syl31anc D∞MetXSXAXBXFAFASAballDFA=
99 95 98 mpbid D∞MetXSXAXBXSAballDFA=
100 sseq0 SBballDFA+𝑒ADBSAballDFASAballDFA=SBballDFA+𝑒ADB=
101 94 99 100 syl2anc D∞MetXSXAXBXSBballDFA+𝑒ADB=
102 1 metdsge D∞MetXSXBXFA+𝑒ADB*FA+𝑒ADBFBSBballDFA+𝑒ADB=
103 7 96 9 73 102 syl31anc D∞MetXSXAXBXFA+𝑒ADBFBSBballDFA+𝑒ADB=
104 101 103 mpbird D∞MetXSXAXBXFA+𝑒ADBFB
105 30 9 ffvelrnd D∞MetXSXAXBXFB0+∞
106 eliccxr FB0+∞FB*
107 105 106 syl D∞MetXSXAXBXFB*
108 elxrge0 FB0+∞FB*0FB
109 108 simprbi FB0+∞0FB
110 105 109 syl D∞MetXSXAXBX0FB
111 xlesubadd FA*ADB*FB*0FAADB−∞0FBFA+𝑒ADBFBFAFB+𝑒ADB
112 33 36 107 61 88 110 111 syl33anc D∞MetXSXAXBXFA+𝑒ADBFBFAFB+𝑒ADB
113 104 112 mpbid D∞MetXSXAXBXFAFB+𝑒ADB
114 xaddcom FB*ADB*FB+𝑒ADB=ADB+𝑒FB
115 107 36 114 syl2anc D∞MetXSXAXBXFB+𝑒ADB=ADB+𝑒FB
116 113 115 breqtrd D∞MetXSXAXBXFAADB+𝑒FB