Metamath Proof Explorer


Theorem stdbdxmet

Description: The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis stdbdmet.1 D=xX,yXifxCyRxCyR
Assertion stdbdxmet C∞MetXR*0<RD∞MetX

Proof

Step Hyp Ref Expression
1 stdbdmet.1 D=xX,yXifxCyRxCyR
2 simp1 C∞MetXR*0<RC∞MetX
3 xmetcl C∞MetXxXyXxCy*
4 xmetge0 C∞MetXxXyX0xCy
5 elxrge0 xCy0+∞xCy*0xCy
6 3 4 5 sylanbrc C∞MetXxXyXxCy0+∞
7 6 3expb C∞MetXxXyXxCy0+∞
8 2 7 sylan C∞MetXR*0<RxXyXxCy0+∞
9 xmetf C∞MetXC:X×X*
10 9 3ad2ant1 C∞MetXR*0<RC:X×X*
11 10 ffnd C∞MetXR*0<RCFnX×X
12 fnov CFnX×XC=xX,yXxCy
13 11 12 sylib C∞MetXR*0<RC=xX,yXxCy
14 eqidd C∞MetXR*0<Rz0+∞ifzRzR=z0+∞ifzRzR
15 breq1 z=xCyzRxCyR
16 id z=xCyz=xCy
17 15 16 ifbieq1d z=xCyifzRzR=ifxCyRxCyR
18 8 13 14 17 fmpoco C∞MetXR*0<Rz0+∞ifzRzRC=xX,yXifxCyRxCyR
19 18 1 eqtr4di C∞MetXR*0<Rz0+∞ifzRzRC=D
20 eliccxr z0+∞z*
21 simp2 C∞MetXR*0<RR*
22 ifcl z*R*ifzRzR*
23 20 21 22 syl2anr C∞MetXR*0<Rz0+∞ifzRzR*
24 23 fmpttd C∞MetXR*0<Rz0+∞ifzRzR:0+∞*
25 id a0+∞a0+∞
26 vex aV
27 ifexg aVR*ifaRaRV
28 26 21 27 sylancr C∞MetXR*0<RifaRaRV
29 breq1 z=azRaR
30 id z=az=a
31 29 30 ifbieq1d z=aifzRzR=ifaRaR
32 eqid z0+∞ifzRzR=z0+∞ifzRzR
33 31 32 fvmptg a0+∞ifaRaRVz0+∞ifzRzRa=ifaRaR
34 25 28 33 syl2anr C∞MetXR*0<Ra0+∞z0+∞ifzRzRa=ifaRaR
35 34 eqeq1d C∞MetXR*0<Ra0+∞z0+∞ifzRzRa=0ifaRaR=0
36 eqeq1 a=ifaRaRa=0ifaRaR=0
37 36 bibi1d a=ifaRaRa=0a=0ifaRaR=0a=0
38 eqeq1 R=ifaRaRR=0ifaRaR=0
39 38 bibi1d R=ifaRaRR=0a=0ifaRaR=0a=0
40 biidd C∞MetXR*0<Ra0+∞aRa=0a=0
41 simp3 C∞MetXR*0<R0<R
42 41 gt0ne0d C∞MetXR*0<RR0
43 42 neneqd C∞MetXR*0<R¬R=0
44 43 ad2antrr C∞MetXR*0<Ra0+∞¬aR¬R=0
45 0xr 0*
46 xrltle 0*R*0<R0R
47 45 21 46 sylancr C∞MetXR*0<R0<R0R
48 41 47 mpd C∞MetXR*0<R0R
49 48 adantr C∞MetXR*0<Ra0+∞0R
50 breq1 a=0aR0R
51 49 50 syl5ibrcom C∞MetXR*0<Ra0+∞a=0aR
52 51 con3dimp C∞MetXR*0<Ra0+∞¬aR¬a=0
53 44 52 2falsed C∞MetXR*0<Ra0+∞¬aRR=0a=0
54 37 39 40 53 ifbothda C∞MetXR*0<Ra0+∞ifaRaR=0a=0
55 35 54 bitrd C∞MetXR*0<Ra0+∞z0+∞ifzRzRa=0a=0
56 eliccxr a0+∞a*
57 56 ad2antrl C∞MetXR*0<Ra0+∞b0+∞a*
58 21 adantr C∞MetXR*0<Ra0+∞b0+∞R*
59 xrmin1 a*R*ifaRaRa
60 57 58 59 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifaRaRa
61 57 58 ifcld C∞MetXR*0<Ra0+∞b0+∞ifaRaR*
62 eliccxr b0+∞b*
63 62 ad2antll C∞MetXR*0<Ra0+∞b0+∞b*
64 xrletr ifaRaR*a*b*ifaRaRaabifaRaRb
65 61 57 63 64 syl3anc C∞MetXR*0<Ra0+∞b0+∞ifaRaRaabifaRaRb
66 60 65 mpand C∞MetXR*0<Ra0+∞b0+∞abifaRaRb
67 xrmin2 a*R*ifaRaRR
68 57 58 67 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifaRaRR
69 66 68 jctird C∞MetXR*0<Ra0+∞b0+∞abifaRaRbifaRaRR
70 xrlemin ifaRaR*b*R*ifaRaRifbRbRifaRaRbifaRaRR
71 61 63 58 70 syl3anc C∞MetXR*0<Ra0+∞b0+∞ifaRaRifbRbRifaRaRbifaRaRR
72 69 71 sylibrd C∞MetXR*0<Ra0+∞b0+∞abifaRaRifbRbR
73 34 adantrr C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRa=ifaRaR
74 simpr a0+∞b0+∞b0+∞
75 vex bV
76 ifexg bVR*ifbRbRV
77 75 21 76 sylancr C∞MetXR*0<RifbRbRV
78 breq1 z=bzRbR
79 id z=bz=b
80 78 79 ifbieq1d z=bifzRzR=ifbRbR
81 80 32 fvmptg b0+∞ifbRbRVz0+∞ifzRzRb=ifbRbR
82 74 77 81 syl2anr C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRb=ifbRbR
83 73 82 breq12d C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRaz0+∞ifzRzRbifaRaRifbRbR
84 72 83 sylibrd C∞MetXR*0<Ra0+∞b0+∞abz0+∞ifzRzRaz0+∞ifzRzRb
85 57 63 xaddcld C∞MetXR*0<Ra0+∞b0+∞a+𝑒b*
86 xrmin1 a+𝑒b*R*ifa+𝑒bRa+𝑒bRa+𝑒b
87 85 58 86 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRa+𝑒b
88 85 58 ifcld C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bR*
89 57 58 xaddcld C∞MetXR*0<Ra0+∞b0+∞a+𝑒R*
90 xrmin2 a+𝑒b*R*ifa+𝑒bRa+𝑒bRR
91 85 58 90 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRR
92 xaddid2 R*0+𝑒R=R
93 58 92 syl C∞MetXR*0<Ra0+∞b0+∞0+𝑒R=R
94 45 a1i C∞MetXR*0<Ra0+∞b0+∞0*
95 elxrge0 a0+∞a*0a
96 95 simprbi a0+∞0a
97 96 ad2antrl C∞MetXR*0<Ra0+∞b0+∞0a
98 xleadd1a 0*a*R*0a0+𝑒Ra+𝑒R
99 94 57 58 97 98 syl31anc C∞MetXR*0<Ra0+∞b0+∞0+𝑒Ra+𝑒R
100 93 99 eqbrtrrd C∞MetXR*0<Ra0+∞b0+∞Ra+𝑒R
101 88 58 89 91 100 xrletrd C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRa+𝑒R
102 oveq2 b=ifbRbRa+𝑒b=a+𝑒ifbRbR
103 102 breq2d b=ifbRbRifa+𝑒bRa+𝑒bRa+𝑒bifa+𝑒bRa+𝑒bRa+𝑒ifbRbR
104 oveq2 R=ifbRbRa+𝑒R=a+𝑒ifbRbR
105 104 breq2d R=ifbRbRifa+𝑒bRa+𝑒bRa+𝑒Rifa+𝑒bRa+𝑒bRa+𝑒ifbRbR
106 103 105 ifboth ifa+𝑒bRa+𝑒bRa+𝑒bifa+𝑒bRa+𝑒bRa+𝑒Rifa+𝑒bRa+𝑒bRa+𝑒ifbRbR
107 87 101 106 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRa+𝑒ifbRbR
108 63 58 ifcld C∞MetXR*0<Ra0+∞b0+∞ifbRbR*
109 58 108 xaddcld C∞MetXR*0<Ra0+∞b0+∞R+𝑒ifbRbR*
110 58 xaddid1d C∞MetXR*0<Ra0+∞b0+∞R+𝑒0=R
111 elxrge0 b0+∞b*0b
112 111 simprbi b0+∞0b
113 112 ad2antll C∞MetXR*0<Ra0+∞b0+∞0b
114 48 adantr C∞MetXR*0<Ra0+∞b0+∞0R
115 breq2 b=ifbRbR0b0ifbRbR
116 breq2 R=ifbRbR0R0ifbRbR
117 115 116 ifboth 0b0R0ifbRbR
118 113 114 117 syl2anc C∞MetXR*0<Ra0+∞b0+∞0ifbRbR
119 xleadd2a 0*ifbRbR*R*0ifbRbRR+𝑒0R+𝑒ifbRbR
120 94 108 58 118 119 syl31anc C∞MetXR*0<Ra0+∞b0+∞R+𝑒0R+𝑒ifbRbR
121 110 120 eqbrtrrd C∞MetXR*0<Ra0+∞b0+∞RR+𝑒ifbRbR
122 88 58 109 91 121 xrletrd C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRR+𝑒ifbRbR
123 oveq1 a=ifaRaRa+𝑒ifbRbR=ifaRaR+𝑒ifbRbR
124 123 breq2d a=ifaRaRifa+𝑒bRa+𝑒bRa+𝑒ifbRbRifa+𝑒bRa+𝑒bRifaRaR+𝑒ifbRbR
125 oveq1 R=ifaRaRR+𝑒ifbRbR=ifaRaR+𝑒ifbRbR
126 125 breq2d R=ifaRaRifa+𝑒bRa+𝑒bRR+𝑒ifbRbRifa+𝑒bRa+𝑒bRifaRaR+𝑒ifbRbR
127 124 126 ifboth ifa+𝑒bRa+𝑒bRa+𝑒ifbRbRifa+𝑒bRa+𝑒bRR+𝑒ifbRbRifa+𝑒bRa+𝑒bRifaRaR+𝑒ifbRbR
128 107 122 127 syl2anc C∞MetXR*0<Ra0+∞b0+∞ifa+𝑒bRa+𝑒bRifaRaR+𝑒ifbRbR
129 ge0xaddcl a0+∞b0+∞a+𝑒b0+∞
130 ovex a+𝑒bV
131 ifexg a+𝑒bVR*ifa+𝑒bRa+𝑒bRV
132 130 21 131 sylancr C∞MetXR*0<Rifa+𝑒bRa+𝑒bRV
133 breq1 z=a+𝑒bzRa+𝑒bR
134 id z=a+𝑒bz=a+𝑒b
135 133 134 ifbieq1d z=a+𝑒bifzRzR=ifa+𝑒bRa+𝑒bR
136 135 32 fvmptg a+𝑒b0+∞ifa+𝑒bRa+𝑒bRVz0+∞ifzRzRa+𝑒b=ifa+𝑒bRa+𝑒bR
137 129 132 136 syl2anr C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRa+𝑒b=ifa+𝑒bRa+𝑒bR
138 73 82 oveq12d C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRa+𝑒z0+∞ifzRzRb=ifaRaR+𝑒ifbRbR
139 128 137 138 3brtr4d C∞MetXR*0<Ra0+∞b0+∞z0+∞ifzRzRa+𝑒bz0+∞ifzRzRa+𝑒z0+∞ifzRzRb
140 2 24 55 84 139 comet C∞MetXR*0<Rz0+∞ifzRzRC∞MetX
141 19 140 eqeltrrd C∞MetXR*0<RD∞MetX