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 = x X , y X if x C y R x C y R
Assertion stdbdxmet C ∞Met X R * 0 < R D ∞Met X

Proof

Step Hyp Ref Expression
1 stdbdmet.1 D = x X , y X if x C y R x C y R
2 simp1 C ∞Met X R * 0 < R C ∞Met X
3 xmetcl C ∞Met X x X y X x C y *
4 xmetge0 C ∞Met X x X y X 0 x C y
5 elxrge0 x C y 0 +∞ x C y * 0 x C y
6 3 4 5 sylanbrc C ∞Met X x X y X x C y 0 +∞
7 6 3expb C ∞Met X x X y X x C y 0 +∞
8 2 7 sylan C ∞Met X R * 0 < R x X y X x C y 0 +∞
9 xmetf C ∞Met X C : X × X *
10 9 3ad2ant1 C ∞Met X R * 0 < R C : X × X *
11 10 ffnd C ∞Met X R * 0 < R C Fn X × X
12 fnov C Fn X × X C = x X , y X x C y
13 11 12 sylib C ∞Met X R * 0 < R C = x X , y X x C y
14 eqidd C ∞Met X R * 0 < R z 0 +∞ if z R z R = z 0 +∞ if z R z R
15 breq1 z = x C y z R x C y R
16 id z = x C y z = x C y
17 15 16 ifbieq1d z = x C y if z R z R = if x C y R x C y R
18 8 13 14 17 fmpoco C ∞Met X R * 0 < R z 0 +∞ if z R z R C = x X , y X if x C y R x C y R
19 18 1 syl6eqr C ∞Met X R * 0 < R z 0 +∞ if z R z R C = D
20 eliccxr z 0 +∞ z *
21 simp2 C ∞Met X R * 0 < R R *
22 ifcl z * R * if z R z R *
23 20 21 22 syl2anr C ∞Met X R * 0 < R z 0 +∞ if z R z R *
24 23 fmpttd C ∞Met X R * 0 < R z 0 +∞ if z R z R : 0 +∞ *
25 id a 0 +∞ a 0 +∞
26 vex a V
27 ifexg a V R * if a R a R V
28 26 21 27 sylancr C ∞Met X R * 0 < R if a R a R V
29 breq1 z = a z R a R
30 id z = a z = a
31 29 30 ifbieq1d z = a if z R z R = if a R a R
32 eqid z 0 +∞ if z R z R = z 0 +∞ if z R z R
33 31 32 fvmptg a 0 +∞ if a R a R V z 0 +∞ if z R z R a = if a R a R
34 25 28 33 syl2anr C ∞Met X R * 0 < R a 0 +∞ z 0 +∞ if z R z R a = if a R a R
35 34 eqeq1d C ∞Met X R * 0 < R a 0 +∞ z 0 +∞ if z R z R a = 0 if a R a R = 0
36 eqeq1 a = if a R a R a = 0 if a R a R = 0
37 36 bibi1d a = if a R a R a = 0 a = 0 if a R a R = 0 a = 0
38 eqeq1 R = if a R a R R = 0 if a R a R = 0
39 38 bibi1d R = if a R a R R = 0 a = 0 if a R a R = 0 a = 0
40 biidd C ∞Met X R * 0 < R a 0 +∞ a R a = 0 a = 0
41 simp3 C ∞Met X R * 0 < R 0 < R
42 41 gt0ne0d C ∞Met X R * 0 < R R 0
43 42 neneqd C ∞Met X R * 0 < R ¬ R = 0
44 43 ad2antrr C ∞Met X R * 0 < R a 0 +∞ ¬ a R ¬ R = 0
45 0xr 0 *
46 xrltle 0 * R * 0 < R 0 R
47 45 21 46 sylancr C ∞Met X R * 0 < R 0 < R 0 R
48 41 47 mpd C ∞Met X R * 0 < R 0 R
49 48 adantr C ∞Met X R * 0 < R a 0 +∞ 0 R
50 breq1 a = 0 a R 0 R
51 49 50 syl5ibrcom C ∞Met X R * 0 < R a 0 +∞ a = 0 a R
52 51 con3dimp C ∞Met X R * 0 < R a 0 +∞ ¬ a R ¬ a = 0
53 44 52 2falsed C ∞Met X R * 0 < R a 0 +∞ ¬ a R R = 0 a = 0
54 37 39 40 53 ifbothda C ∞Met X R * 0 < R a 0 +∞ if a R a R = 0 a = 0
55 35 54 bitrd C ∞Met X R * 0 < R a 0 +∞ z 0 +∞ if z R z R a = 0 a = 0
56 eliccxr a 0 +∞ a *
57 56 ad2antrl C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a *
58 21 adantr C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R *
59 xrmin1 a * R * if a R a R a
60 57 58 59 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a R a R a
61 57 58 ifcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a R a R *
62 eliccxr b 0 +∞ b *
63 62 ad2antll C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ b *
64 xrletr if a R a R * a * b * if a R a R a a b if a R a R b
65 61 57 63 64 syl3anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a R a R a a b if a R a R b
66 60 65 mpand C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a b if a R a R b
67 xrmin2 a * R * if a R a R R
68 57 58 67 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a R a R R
69 66 68 jctird C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a b if a R a R b if a R a R R
70 xrlemin if a R a R * b * R * if a R a R if b R b R if a R a R b if a R a R R
71 61 63 58 70 syl3anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a R a R if b R b R if a R a R b if a R a R R
72 69 71 sylibrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a b if a R a R if b R b R
73 34 adantrr C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R a = if a R a R
74 simpr a 0 +∞ b 0 +∞ b 0 +∞
75 vex b V
76 ifexg b V R * if b R b R V
77 75 21 76 sylancr C ∞Met X R * 0 < R if b R b R V
78 breq1 z = b z R b R
79 id z = b z = b
80 78 79 ifbieq1d z = b if z R z R = if b R b R
81 80 32 fvmptg b 0 +∞ if b R b R V z 0 +∞ if z R z R b = if b R b R
82 74 77 81 syl2anr C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R b = if b R b R
83 73 82 breq12d C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R a z 0 +∞ if z R z R b if a R a R if b R b R
84 72 83 sylibrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a b z 0 +∞ if z R z R a z 0 +∞ if z R z R b
85 57 63 xaddcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a + 𝑒 b *
86 xrmin1 a + 𝑒 b * R * if a + 𝑒 b R a + 𝑒 b R a + 𝑒 b
87 85 58 86 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R a + 𝑒 b
88 85 58 ifcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R *
89 57 58 xaddcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ a + 𝑒 R *
90 xrmin2 a + 𝑒 b * R * if a + 𝑒 b R a + 𝑒 b R R
91 85 58 90 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R R
92 xaddid2 R * 0 + 𝑒 R = R
93 58 92 syl C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 + 𝑒 R = R
94 45 a1i C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 *
95 elxrge0 a 0 +∞ a * 0 a
96 95 simprbi a 0 +∞ 0 a
97 96 ad2antrl C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 a
98 xleadd1a 0 * a * R * 0 a 0 + 𝑒 R a + 𝑒 R
99 94 57 58 97 98 syl31anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 + 𝑒 R a + 𝑒 R
100 93 99 eqbrtrrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R a + 𝑒 R
101 88 58 89 91 100 xrletrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R a + 𝑒 R
102 oveq2 b = if b R b R a + 𝑒 b = a + 𝑒 if b R b R
103 102 breq2d b = if b R b R if a + 𝑒 b R a + 𝑒 b R a + 𝑒 b if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R
104 oveq2 R = if b R b R a + 𝑒 R = a + 𝑒 if b R b R
105 104 breq2d R = if b R b R if a + 𝑒 b R a + 𝑒 b R a + 𝑒 R if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R
106 103 105 ifboth if a + 𝑒 b R a + 𝑒 b R a + 𝑒 b if a + 𝑒 b R a + 𝑒 b R a + 𝑒 R if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R
107 87 101 106 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R
108 63 58 ifcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if b R b R *
109 58 108 xaddcld C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R + 𝑒 if b R b R *
110 58 xaddid1d C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R + 𝑒 0 = R
111 elxrge0 b 0 +∞ b * 0 b
112 111 simprbi b 0 +∞ 0 b
113 112 ad2antll C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 b
114 48 adantr C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 R
115 breq2 b = if b R b R 0 b 0 if b R b R
116 breq2 R = if b R b R 0 R 0 if b R b R
117 115 116 ifboth 0 b 0 R 0 if b R b R
118 113 114 117 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ 0 if b R b R
119 xleadd2a 0 * if b R b R * R * 0 if b R b R R + 𝑒 0 R + 𝑒 if b R b R
120 94 108 58 118 119 syl31anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R + 𝑒 0 R + 𝑒 if b R b R
121 110 120 eqbrtrrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ R R + 𝑒 if b R b R
122 88 58 109 91 121 xrletrd C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R R + 𝑒 if b R b R
123 oveq1 a = if a R a R a + 𝑒 if b R b R = if a R a R + 𝑒 if b R b R
124 123 breq2d a = if a R a R if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R if a + 𝑒 b R a + 𝑒 b R if a R a R + 𝑒 if b R b R
125 oveq1 R = if a R a R R + 𝑒 if b R b R = if a R a R + 𝑒 if b R b R
126 125 breq2d R = if a R a R if a + 𝑒 b R a + 𝑒 b R R + 𝑒 if b R b R if a + 𝑒 b R a + 𝑒 b R if a R a R + 𝑒 if b R b R
127 124 126 ifboth if a + 𝑒 b R a + 𝑒 b R a + 𝑒 if b R b R if a + 𝑒 b R a + 𝑒 b R R + 𝑒 if b R b R if a + 𝑒 b R a + 𝑒 b R if a R a R + 𝑒 if b R b R
128 107 122 127 syl2anc C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ if a + 𝑒 b R a + 𝑒 b R if a R a R + 𝑒 if b R b R
129 ge0xaddcl a 0 +∞ b 0 +∞ a + 𝑒 b 0 +∞
130 ovex a + 𝑒 b V
131 ifexg a + 𝑒 b V R * if a + 𝑒 b R a + 𝑒 b R V
132 130 21 131 sylancr C ∞Met X R * 0 < R if a + 𝑒 b R a + 𝑒 b R V
133 breq1 z = a + 𝑒 b z R a + 𝑒 b R
134 id z = a + 𝑒 b z = a + 𝑒 b
135 133 134 ifbieq1d z = a + 𝑒 b if z R z R = if a + 𝑒 b R a + 𝑒 b R
136 135 32 fvmptg a + 𝑒 b 0 +∞ if a + 𝑒 b R a + 𝑒 b R V z 0 +∞ if z R z R a + 𝑒 b = if a + 𝑒 b R a + 𝑒 b R
137 129 132 136 syl2anr C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R a + 𝑒 b = if a + 𝑒 b R a + 𝑒 b R
138 73 82 oveq12d C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R a + 𝑒 z 0 +∞ if z R z R b = if a R a R + 𝑒 if b R b R
139 128 137 138 3brtr4d C ∞Met X R * 0 < R a 0 +∞ b 0 +∞ z 0 +∞ if z R z R a + 𝑒 b z 0 +∞ if z R z R a + 𝑒 z 0 +∞ if z R z R b
140 2 24 55 84 139 comet C ∞Met X R * 0 < R z 0 +∞ if z R z R C ∞Met X
141 19 140 eqeltrrd C ∞Met X R * 0 < R D ∞Met X