Metamath Proof Explorer


Theorem ubthlem2

Description: Lemma for ubth . Given that there is a closed ball B ( P , R ) in AK , for any x e. B ( 0 , 1 ) , we have P + R x. x e. B ( P , R ) and P e. B ( P , R ) , so both of these have norm ( t ( z ) ) <_ K and so norm ( t ( x ) ) <_ ( norm ( t ( P ) ) + norm ( t ( P + R x. x ) ) ) / R <_ ( K + K ) / R , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ubth.1 X = BaseSet U
ubth.2 N = norm CV W
ubthlem.3 D = IndMet U
ubthlem.4 J = MetOpen D
ubthlem.5 U CBan
ubthlem.6 W NrmCVec
ubthlem.7 φ T U BLnOp W
ubthlem.8 φ x X c t T N t x c
ubthlem.9 A = k z X | t T N t z k
ubthlem.10 φ K
ubthlem.11 φ P X
ubthlem.12 φ R +
ubthlem.13 φ z X | P D z R A K
Assertion ubthlem2 φ d t T U normOp OLD W t d

Proof

Step Hyp Ref Expression
1 ubth.1 X = BaseSet U
2 ubth.2 N = norm CV W
3 ubthlem.3 D = IndMet U
4 ubthlem.4 J = MetOpen D
5 ubthlem.5 U CBan
6 ubthlem.6 W NrmCVec
7 ubthlem.7 φ T U BLnOp W
8 ubthlem.8 φ x X c t T N t x c
9 ubthlem.9 A = k z X | t T N t z k
10 ubthlem.10 φ K
11 ubthlem.11 φ P X
12 ubthlem.12 φ R +
13 ubthlem.13 φ z X | P D z R A K
14 10 nnrpd φ K +
15 14 14 rpaddcld φ K + K +
16 15 12 rpdivcld φ K + K R +
17 16 rpred φ K + K R
18 oveq2 z = P + v U R 𝑠OLD U x P D z = P D P + v U R 𝑠OLD U x
19 18 breq1d z = P + v U R 𝑠OLD U x P D z R P D P + v U R 𝑠OLD U x R
20 eleq1 z = P + v U R 𝑠OLD U x z A K P + v U R 𝑠OLD U x A K
21 19 20 imbi12d z = P + v U R 𝑠OLD U x P D z R z A K P D P + v U R 𝑠OLD U x R P + v U R 𝑠OLD U x A K
22 rabss z X | P D z R A K z X P D z R z A K
23 13 22 sylib φ z X P D z R z A K
24 23 ad2antrr φ t T x X z X P D z R z A K
25 bnnv U CBan U NrmCVec
26 5 25 ax-mp U NrmCVec
27 26 a1i φ t T x X U NrmCVec
28 11 ad2antrr φ t T x X P X
29 12 ad2antrr φ t T x X R +
30 29 rpcnd φ t T x X R
31 simpr φ t T x X x X
32 eqid 𝑠OLD U = 𝑠OLD U
33 1 32 nvscl U NrmCVec R x X R 𝑠OLD U x X
34 27 30 31 33 syl3anc φ t T x X R 𝑠OLD U x X
35 eqid + v U = + v U
36 1 35 nvgcl U NrmCVec P X R 𝑠OLD U x X P + v U R 𝑠OLD U x X
37 27 28 34 36 syl3anc φ t T x X P + v U R 𝑠OLD U x X
38 21 24 37 rspcdva φ t T x X P D P + v U R 𝑠OLD U x R P + v U R 𝑠OLD U x A K
39 1 3 cbncms U CBan D CMet X
40 5 39 ax-mp D CMet X
41 cmetmet D CMet X D Met X
42 metxmet D Met X D ∞Met X
43 40 41 42 mp2b D ∞Met X
44 43 a1i φ t T x X D ∞Met X
45 xmetsym D ∞Met X P X P + v U R 𝑠OLD U x X P D P + v U R 𝑠OLD U x = P + v U R 𝑠OLD U x D P
46 44 28 37 45 syl3anc φ t T x X P D P + v U R 𝑠OLD U x = P + v U R 𝑠OLD U x D P
47 eqid - v U = - v U
48 eqid norm CV U = norm CV U
49 1 47 48 3 imsdval U NrmCVec P + v U R 𝑠OLD U x X P X P + v U R 𝑠OLD U x D P = norm CV U P + v U R 𝑠OLD U x - v U P
50 27 37 28 49 syl3anc φ t T x X P + v U R 𝑠OLD U x D P = norm CV U P + v U R 𝑠OLD U x - v U P
51 1 35 47 nvpncan2 U NrmCVec P X R 𝑠OLD U x X P + v U R 𝑠OLD U x - v U P = R 𝑠OLD U x
52 27 28 34 51 syl3anc φ t T x X P + v U R 𝑠OLD U x - v U P = R 𝑠OLD U x
53 52 fveq2d φ t T x X norm CV U P + v U R 𝑠OLD U x - v U P = norm CV U R 𝑠OLD U x
54 46 50 53 3eqtrd φ t T x X P D P + v U R 𝑠OLD U x = norm CV U R 𝑠OLD U x
55 29 rprege0d φ t T x X R 0 R
56 1 32 48 nvsge0 U NrmCVec R 0 R x X norm CV U R 𝑠OLD U x = R norm CV U x
57 27 55 31 56 syl3anc φ t T x X norm CV U R 𝑠OLD U x = R norm CV U x
58 54 57 eqtrd φ t T x X P D P + v U R 𝑠OLD U x = R norm CV U x
59 30 mulid1d φ t T x X R 1 = R
60 59 eqcomd φ t T x X R = R 1
61 58 60 breq12d φ t T x X P D P + v U R 𝑠OLD U x R R norm CV U x R 1
62 1 48 nvcl U NrmCVec x X norm CV U x
63 26 62 mpan x X norm CV U x
64 63 adantl φ t T x X norm CV U x
65 1red φ t T x X 1
66 64 65 29 lemul2d φ t T x X norm CV U x 1 R norm CV U x R 1
67 61 66 bitr4d φ t T x X P D P + v U R 𝑠OLD U x R norm CV U x 1
68 breq2 k = K N t z k N t z K
69 68 ralbidv k = K t T N t z k t T N t z K
70 69 rabbidv k = K z X | t T N t z k = z X | t T N t z K
71 1 fvexi X V
72 71 rabex z X | t T N t z K V
73 70 9 72 fvmpt K A K = z X | t T N t z K
74 10 73 syl φ A K = z X | t T N t z K
75 74 eleq2d φ P + v U R 𝑠OLD U x A K P + v U R 𝑠OLD U x z X | t T N t z K
76 2fveq3 z = P + v U R 𝑠OLD U x N t z = N t P + v U R 𝑠OLD U x
77 76 breq1d z = P + v U R 𝑠OLD U x N t z K N t P + v U R 𝑠OLD U x K
78 77 ralbidv z = P + v U R 𝑠OLD U x t T N t z K t T N t P + v U R 𝑠OLD U x K
79 78 elrab P + v U R 𝑠OLD U x z X | t T N t z K P + v U R 𝑠OLD U x X t T N t P + v U R 𝑠OLD U x K
80 75 79 bitrdi φ P + v U R 𝑠OLD U x A K P + v U R 𝑠OLD U x X t T N t P + v U R 𝑠OLD U x K
81 80 ad2antrr φ t T x X P + v U R 𝑠OLD U x A K P + v U R 𝑠OLD U x X t T N t P + v U R 𝑠OLD U x K
82 38 67 81 3imtr3d φ t T x X norm CV U x 1 P + v U R 𝑠OLD U x X t T N t P + v U R 𝑠OLD U x K
83 rsp t T N t P + v U R 𝑠OLD U x K t T N t P + v U R 𝑠OLD U x K
84 83 com12 t T t T N t P + v U R 𝑠OLD U x K N t P + v U R 𝑠OLD U x K
85 84 ad2antlr φ t T x X t T N t P + v U R 𝑠OLD U x K N t P + v U R 𝑠OLD U x K
86 xmet0 D ∞Met X P X P D P = 0
87 43 11 86 sylancr φ P D P = 0
88 12 rpge0d φ 0 R
89 87 88 eqbrtrd φ P D P R
90 oveq2 z = P P D z = P D P
91 90 breq1d z = P P D z R P D P R
92 91 elrab P z X | P D z R P X P D P R
93 11 89 92 sylanbrc φ P z X | P D z R
94 13 93 sseldd φ P A K
95 94 74 eleqtrd φ P z X | t T N t z K
96 2fveq3 z = P N t z = N t P
97 96 breq1d z = P N t z K N t P K
98 97 ralbidv z = P t T N t z K t T N t P K
99 98 elrab P z X | t T N t z K P X t T N t P K
100 95 99 sylib φ P X t T N t P K
101 100 simprd φ t T N t P K
102 101 r19.21bi φ t T N t P K
103 102 adantr φ t T x X N t P K
104 7 sselda φ t T t U BLnOp W
105 eqid IndMet W = IndMet W
106 eqid MetOpen IndMet W = MetOpen IndMet W
107 eqid U BLnOp W = U BLnOp W
108 3 105 4 106 107 26 6 blocn2 t U BLnOp W t J Cn MetOpen IndMet W
109 4 mopntopon D ∞Met X J TopOn X
110 43 109 ax-mp J TopOn X
111 eqid BaseSet W = BaseSet W
112 111 105 imsxmet W NrmCVec IndMet W ∞Met BaseSet W
113 106 mopntopon IndMet W ∞Met BaseSet W MetOpen IndMet W TopOn BaseSet W
114 6 112 113 mp2b MetOpen IndMet W TopOn BaseSet W
115 iscncl J TopOn X MetOpen IndMet W TopOn BaseSet W t J Cn MetOpen IndMet W t : X BaseSet W x Clsd MetOpen IndMet W t -1 x Clsd J
116 110 114 115 mp2an t J Cn MetOpen IndMet W t : X BaseSet W x Clsd MetOpen IndMet W t -1 x Clsd J
117 108 116 sylib t U BLnOp W t : X BaseSet W x Clsd MetOpen IndMet W t -1 x Clsd J
118 104 117 syl φ t T t : X BaseSet W x Clsd MetOpen IndMet W t -1 x Clsd J
119 118 simpld φ t T t : X BaseSet W
120 119 adantr φ t T x X t : X BaseSet W
121 120 37 ffvelrnd φ t T x X t P + v U R 𝑠OLD U x BaseSet W
122 111 2 nvcl W NrmCVec t P + v U R 𝑠OLD U x BaseSet W N t P + v U R 𝑠OLD U x
123 6 121 122 sylancr φ t T x X N t P + v U R 𝑠OLD U x
124 120 28 ffvelrnd φ t T x X t P BaseSet W
125 111 2 nvcl W NrmCVec t P BaseSet W N t P
126 6 124 125 sylancr φ t T x X N t P
127 10 nnred φ K
128 127 ad2antrr φ t T x X K
129 le2add N t P + v U R 𝑠OLD U x N t P K K N t P + v U R 𝑠OLD U x K N t P K N t P + v U R 𝑠OLD U x + N t P K + K
130 123 126 128 128 129 syl22anc φ t T x X N t P + v U R 𝑠OLD U x K N t P K N t P + v U R 𝑠OLD U x + N t P K + K
131 103 130 mpan2d φ t T x X N t P + v U R 𝑠OLD U x K N t P + v U R 𝑠OLD U x + N t P K + K
132 52 fveq2d φ t T x X t P + v U R 𝑠OLD U x - v U P = t R 𝑠OLD U x
133 6 a1i φ t T x X W NrmCVec
134 eqid U LnOp W = U LnOp W
135 134 107 bloln U NrmCVec W NrmCVec t U BLnOp W t U LnOp W
136 26 6 135 mp3an12 t U BLnOp W t U LnOp W
137 104 136 syl φ t T t U LnOp W
138 137 adantr φ t T x X t U LnOp W
139 eqid - v W = - v W
140 1 47 139 134 lnosub U NrmCVec W NrmCVec t U LnOp W P + v U R 𝑠OLD U x X P X t P + v U R 𝑠OLD U x - v U P = t P + v U R 𝑠OLD U x - v W t P
141 27 133 138 37 28 140 syl32anc φ t T x X t P + v U R 𝑠OLD U x - v U P = t P + v U R 𝑠OLD U x - v W t P
142 eqid 𝑠OLD W = 𝑠OLD W
143 1 32 142 134 lnomul U NrmCVec W NrmCVec t U LnOp W R x X t R 𝑠OLD U x = R 𝑠OLD W t x
144 27 133 138 30 31 143 syl32anc φ t T x X t R 𝑠OLD U x = R 𝑠OLD W t x
145 132 141 144 3eqtr3d φ t T x X t P + v U R 𝑠OLD U x - v W t P = R 𝑠OLD W t x
146 145 fveq2d φ t T x X N t P + v U R 𝑠OLD U x - v W t P = N R 𝑠OLD W t x
147 119 ffvelrnda φ t T x X t x BaseSet W
148 111 142 2 nvsge0 W NrmCVec R 0 R t x BaseSet W N R 𝑠OLD W t x = R N t x
149 133 55 147 148 syl3anc φ t T x X N R 𝑠OLD W t x = R N t x
150 146 149 eqtrd φ t T x X N t P + v U R 𝑠OLD U x - v W t P = R N t x
151 111 139 2 nvmtri W NrmCVec t P + v U R 𝑠OLD U x BaseSet W t P BaseSet W N t P + v U R 𝑠OLD U x - v W t P N t P + v U R 𝑠OLD U x + N t P
152 133 121 124 151 syl3anc φ t T x X N t P + v U R 𝑠OLD U x - v W t P N t P + v U R 𝑠OLD U x + N t P
153 150 152 eqbrtrrd φ t T x X R N t x N t P + v U R 𝑠OLD U x + N t P
154 29 rpred φ t T x X R
155 111 2 nvcl W NrmCVec t x BaseSet W N t x
156 6 147 155 sylancr φ t T x X N t x
157 154 156 remulcld φ t T x X R N t x
158 123 126 readdcld φ t T x X N t P + v U R 𝑠OLD U x + N t P
159 15 rpred φ K + K
160 159 ad2antrr φ t T x X K + K
161 letr R N t x N t P + v U R 𝑠OLD U x + N t P K + K R N t x N t P + v U R 𝑠OLD U x + N t P N t P + v U R 𝑠OLD U x + N t P K + K R N t x K + K
162 157 158 160 161 syl3anc φ t T x X R N t x N t P + v U R 𝑠OLD U x + N t P N t P + v U R 𝑠OLD U x + N t P K + K R N t x K + K
163 153 162 mpand φ t T x X N t P + v U R 𝑠OLD U x + N t P K + K R N t x K + K
164 131 163 syld φ t T x X N t P + v U R 𝑠OLD U x K R N t x K + K
165 156 160 29 lemuldiv2d φ t T x X R N t x K + K N t x K + K R
166 164 165 sylibd φ t T x X N t P + v U R 𝑠OLD U x K N t x K + K R
167 85 166 syld φ t T x X t T N t P + v U R 𝑠OLD U x K N t x K + K R
168 167 adantld φ t T x X P + v U R 𝑠OLD U x X t T N t P + v U R 𝑠OLD U x K N t x K + K R
169 82 168 syld φ t T x X norm CV U x 1 N t x K + K R
170 169 ralrimiva φ t T x X norm CV U x 1 N t x K + K R
171 16 rpxrd φ K + K R *
172 171 adantr φ t T K + K R *
173 eqid U normOp OLD W = U normOp OLD W
174 1 111 48 2 173 26 6 nmoubi t : X BaseSet W K + K R * U normOp OLD W t K + K R x X norm CV U x 1 N t x K + K R
175 119 172 174 syl2anc φ t T U normOp OLD W t K + K R x X norm CV U x 1 N t x K + K R
176 170 175 mpbird φ t T U normOp OLD W t K + K R
177 176 ralrimiva φ t T U normOp OLD W t K + K R
178 brralrspcev K + K R t T U normOp OLD W t K + K R d t T U normOp OLD W t d
179 17 177 178 syl2anc φ d t T U normOp OLD W t d