Metamath Proof Explorer


Theorem fourierdlem54

Description: Given a partition Q and an arbitrary interval [ C , D ] , a partition S on [ C , D ] is built such that it preserves any periodic function piecewise continuous on Q will be piecewise continuous on S , with the same limits. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem54.t T = B A
fourierdlem54.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem54.m φ M
fourierdlem54.q φ Q P M
fourierdlem54.c φ C
fourierdlem54.d φ D
fourierdlem54.cd φ C < D
fourierdlem54.o O = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
fourierdlem54.h H = C D x C D | k x + k T ran Q
fourierdlem54.n N = H 1
fourierdlem54.s S = ι f | f Isom < , < 0 N H
Assertion fourierdlem54 φ N S O N S Isom < , < 0 N H

Proof

Step Hyp Ref Expression
1 fourierdlem54.t T = B A
2 fourierdlem54.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
3 fourierdlem54.m φ M
4 fourierdlem54.q φ Q P M
5 fourierdlem54.c φ C
6 fourierdlem54.d φ D
7 fourierdlem54.cd φ C < D
8 fourierdlem54.o O = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
9 fourierdlem54.h H = C D x C D | k x + k T ran Q
10 fourierdlem54.n N = H 1
11 fourierdlem54.s S = ι f | f Isom < , < 0 N H
12 2z 2
13 12 a1i φ 2
14 prid1g C C C D
15 elun1 C C D C C D x C D | k x + k T ran Q
16 5 14 15 3syl φ C C D x C D | k x + k T ran Q
17 16 9 eleqtrrdi φ C H
18 17 ne0d φ H
19 prfi C D Fin
20 2 3 4 fourierdlem11 φ A B A < B
21 20 simp1d φ A
22 20 simp2d φ B
23 20 simp3d φ A < B
24 2 3 4 fourierdlem15 φ Q : 0 M A B
25 frn Q : 0 M A B ran Q A B
26 24 25 syl φ ran Q A B
27 2 fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
28 3 27 syl φ Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
29 4 28 mpbid φ Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
30 29 simpld φ Q 0 M
31 elmapi Q 0 M Q : 0 M
32 ffn Q : 0 M Q Fn 0 M
33 30 31 32 3syl φ Q Fn 0 M
34 fzfid φ 0 M Fin
35 fnfi Q Fn 0 M 0 M Fin Q Fin
36 33 34 35 syl2anc φ Q Fin
37 rnfi Q Fin ran Q Fin
38 36 37 syl φ ran Q Fin
39 29 simprd φ Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
40 39 simpld φ Q 0 = A Q M = B
41 40 simpld φ Q 0 = A
42 3 nnnn0d φ M 0
43 nn0uz 0 = 0
44 42 43 eleqtrdi φ M 0
45 eluzfz1 M 0 0 0 M
46 44 45 syl φ 0 0 M
47 fnfvelrn Q Fn 0 M 0 0 M Q 0 ran Q
48 33 46 47 syl2anc φ Q 0 ran Q
49 41 48 eqeltrrd φ A ran Q
50 40 simprd φ Q M = B
51 eluzfz2 M 0 M 0 M
52 44 51 syl φ M 0 M
53 fnfvelrn Q Fn 0 M M 0 M Q M ran Q
54 33 52 53 syl2anc φ Q M ran Q
55 50 54 eqeltrrd φ B ran Q
56 eqid abs = abs
57 eqid ran Q × ran Q I = ran Q × ran Q I
58 eqid ran abs ran Q × ran Q I = ran abs ran Q × ran Q I
59 eqid sup ran abs ran Q × ran Q I < = sup ran abs ran Q × ran Q I <
60 eqid topGen ran . = topGen ran .
61 eqid topGen ran . 𝑡 C D = topGen ran . 𝑡 C D
62 oveq1 x = w x + k T = w + k T
63 62 eleq1d x = w x + k T ran Q w + k T ran Q
64 63 rexbidv x = w k x + k T ran Q k w + k T ran Q
65 64 cbvrabv x C D | k x + k T ran Q = w C D | k w + k T ran Q
66 oveq1 i = j i T = j T
67 66 oveq2d i = j y + i T = y + j T
68 67 eleq1d i = j y + i T ran Q y + j T ran Q
69 68 anbi1d i = j y + i T ran Q z + l T ran Q y + j T ran Q z + l T ran Q
70 oveq1 l = k l T = k T
71 70 oveq2d l = k z + l T = z + k T
72 71 eleq1d l = k z + l T ran Q z + k T ran Q
73 72 anbi2d l = k y + j T ran Q z + l T ran Q y + j T ran Q z + k T ran Q
74 69 73 cbvrex2vw i l y + i T ran Q z + l T ran Q j k y + j T ran Q z + k T ran Q
75 74 anbi2i φ y z y < z i l y + i T ran Q z + l T ran Q φ y z y < z j k y + j T ran Q z + k T ran Q
76 21 22 23 1 26 38 49 55 56 57 58 59 5 6 60 61 65 75 fourierdlem42 φ x C D | k x + k T ran Q Fin
77 unfi C D Fin x C D | k x + k T ran Q Fin C D x C D | k x + k T ran Q Fin
78 19 76 77 sylancr φ C D x C D | k x + k T ran Q Fin
79 9 78 eqeltrid φ H Fin
80 hashnncl H Fin H H
81 79 80 syl φ H H
82 18 81 mpbird φ H
83 82 nnzd φ H
84 5 7 ltned φ C D
85 hashprg C D C D C D = 2
86 5 6 85 syl2anc φ C D C D = 2
87 84 86 mpbid φ C D = 2
88 87 eqcomd φ 2 = C D
89 ssun1 C D C D x C D | k x + k T ran Q
90 89 a1i φ C D C D x C D | k x + k T ran Q
91 90 9 sseqtrrdi φ C D H
92 hashssle H Fin C D H C D H
93 79 91 92 syl2anc φ C D H
94 88 93 eqbrtrd φ 2 H
95 eluz2 H 2 2 H 2 H
96 13 83 94 95 syl3anbrc φ H 2
97 uz2m1nn H 2 H 1
98 96 97 syl φ H 1
99 10 98 eqeltrid φ N
100 prssg C D C D C D
101 5 6 100 syl2anc φ C D C D
102 5 6 101 mpbi2and φ C D
103 ssrab2 x C D | k x + k T ran Q C D
104 5 6 iccssred φ C D
105 103 104 sstrid φ x C D | k x + k T ran Q
106 102 105 unssd φ C D x C D | k x + k T ran Q
107 9 106 eqsstrid φ H
108 79 107 11 10 fourierdlem36 φ S Isom < , < 0 N H
109 df-isom S Isom < , < 0 N H S : 0 N 1-1 onto H x 0 N y 0 N x < y S x < S y
110 108 109 sylib φ S : 0 N 1-1 onto H x 0 N y 0 N x < y S x < S y
111 110 simpld φ S : 0 N 1-1 onto H
112 f1of S : 0 N 1-1 onto H S : 0 N H
113 111 112 syl φ S : 0 N H
114 113 107 fssd φ S : 0 N
115 reex V
116 ovex 0 N V
117 116 a1i φ 0 N V
118 elmapg V 0 N V S 0 N S : 0 N
119 115 117 118 sylancr φ S 0 N S : 0 N
120 114 119 mpbird φ S 0 N
121 df-f1o S : 0 N 1-1 onto H S : 0 N 1-1 H S : 0 N onto H
122 111 121 sylib φ S : 0 N 1-1 H S : 0 N onto H
123 122 simprd φ S : 0 N onto H
124 dffo3 S : 0 N onto H S : 0 N H h H y 0 N h = S y
125 123 124 sylib φ S : 0 N H h H y 0 N h = S y
126 125 simprd φ h H y 0 N h = S y
127 eqeq1 h = C h = S y C = S y
128 eqcom C = S y S y = C
129 127 128 bitrdi h = C h = S y S y = C
130 129 rexbidv h = C y 0 N h = S y y 0 N S y = C
131 130 rspcv C H h H y 0 N h = S y y 0 N S y = C
132 17 126 131 sylc φ y 0 N S y = C
133 fveq2 y = 0 S y = S 0
134 133 eqcomd y = 0 S 0 = S y
135 134 adantl φ S y = C y = 0 S 0 = S y
136 simplr φ S y = C y = 0 S y = C
137 135 136 eqtrd φ S y = C y = 0 S 0 = C
138 5 ad2antrr φ S y = C y = 0 C
139 137 138 eqeltrd φ S y = C y = 0 S 0
140 139 137 eqled φ S y = C y = 0 S 0 C
141 140 3adantl2 φ y 0 N S y = C y = 0 S 0 C
142 5 rexrd φ C *
143 6 rexrd φ D *
144 5 6 7 ltled φ C D
145 lbicc2 C * D * C D C C D
146 142 143 144 145 syl3anc φ C C D
147 ubicc2 C * D * C D D C D
148 142 143 144 147 syl3anc φ D C D
149 prssg C C D D C D C C D D C D C D C D
150 146 148 149 syl2anc φ C C D D C D C D C D
151 146 148 150 mpbi2and φ C D C D
152 103 a1i φ x C D | k x + k T ran Q C D
153 151 152 unssd φ C D x C D | k x + k T ran Q C D
154 9 153 eqsstrid φ H C D
155 nnm1nn0 H H 1 0
156 82 155 syl φ H 1 0
157 10 156 eqeltrid φ N 0
158 157 43 eleqtrdi φ N 0
159 eluzfz1 N 0 0 0 N
160 158 159 syl φ 0 0 N
161 113 160 ffvelrnd φ S 0 H
162 154 161 sseldd φ S 0 C D
163 104 162 sseldd φ S 0
164 163 adantr φ ¬ y = 0 S 0
165 164 3ad2antl1 φ y 0 N S y = C ¬ y = 0 S 0
166 5 adantr φ ¬ y = 0 C
167 166 3ad2antl1 φ y 0 N S y = C ¬ y = 0 C
168 elfzelz y 0 N y
169 168 zred y 0 N y
170 169 adantr y 0 N ¬ y = 0 y
171 elfzle1 y 0 N 0 y
172 171 adantr y 0 N ¬ y = 0 0 y
173 neqne ¬ y = 0 y 0
174 173 adantl y 0 N ¬ y = 0 y 0
175 170 172 174 ne0gt0d y 0 N ¬ y = 0 0 < y
176 175 3ad2antl2 φ y 0 N S y = C ¬ y = 0 0 < y
177 simpl1 φ y 0 N S y = C ¬ y = 0 φ
178 simpl2 φ y 0 N S y = C ¬ y = 0 y 0 N
179 110 simprd φ x 0 N y 0 N x < y S x < S y
180 breq1 x = 0 x < y 0 < y
181 fveq2 x = 0 S x = S 0
182 181 breq1d x = 0 S x < S y S 0 < S y
183 180 182 bibi12d x = 0 x < y S x < S y 0 < y S 0 < S y
184 183 ralbidv x = 0 y 0 N x < y S x < S y y 0 N 0 < y S 0 < S y
185 184 rspcv 0 0 N x 0 N y 0 N x < y S x < S y y 0 N 0 < y S 0 < S y
186 160 179 185 sylc φ y 0 N 0 < y S 0 < S y
187 186 r19.21bi φ y 0 N 0 < y S 0 < S y
188 177 178 187 syl2anc φ y 0 N S y = C ¬ y = 0 0 < y S 0 < S y
189 176 188 mpbid φ y 0 N S y = C ¬ y = 0 S 0 < S y
190 simpl3 φ y 0 N S y = C ¬ y = 0 S y = C
191 189 190 breqtrd φ y 0 N S y = C ¬ y = 0 S 0 < C
192 165 167 191 ltled φ y 0 N S y = C ¬ y = 0 S 0 C
193 141 192 pm2.61dan φ y 0 N S y = C S 0 C
194 193 rexlimdv3a φ y 0 N S y = C S 0 C
195 132 194 mpd φ S 0 C
196 elicc2 C D S 0 C D S 0 C S 0 S 0 D
197 5 6 196 syl2anc φ S 0 C D S 0 C S 0 S 0 D
198 162 197 mpbid φ S 0 C S 0 S 0 D
199 198 simp2d φ C S 0
200 163 5 letri3d φ S 0 = C S 0 C C S 0
201 195 199 200 mpbir2and φ S 0 = C
202 eluzfz2 N 0 N 0 N
203 158 202 syl φ N 0 N
204 113 203 ffvelrnd φ S N H
205 154 204 sseldd φ S N C D
206 elicc2 C D S N C D S N C S N S N D
207 5 6 206 syl2anc φ S N C D S N C S N S N D
208 205 207 mpbid φ S N C S N S N D
209 208 simp3d φ S N D
210 prid2g D D C D
211 elun1 D C D D C D x C D | k x + k T ran Q
212 6 210 211 3syl φ D C D x C D | k x + k T ran Q
213 212 9 eleqtrrdi φ D H
214 eqeq1 h = D h = S y D = S y
215 eqcom D = S y S y = D
216 214 215 bitrdi h = D h = S y S y = D
217 216 rexbidv h = D y 0 N h = S y y 0 N S y = D
218 217 rspcv D H h H y 0 N h = S y y 0 N S y = D
219 213 126 218 sylc φ y 0 N S y = D
220 215 biimpri S y = D D = S y
221 220 3ad2ant3 φ y 0 N S y = D D = S y
222 114 ffvelrnda φ y 0 N S y
223 104 205 sseldd φ S N
224 223 adantr φ y 0 N S N
225 169 adantl φ y 0 N y
226 elfzel2 y 0 N N
227 226 zred y 0 N N
228 227 adantl φ y 0 N N
229 elfzle2 y 0 N y N
230 229 adantl φ y 0 N y N
231 225 228 230 lensymd φ y 0 N ¬ N < y
232 breq1 x = N x < y N < y
233 fveq2 x = N S x = S N
234 233 breq1d x = N S x < S y S N < S y
235 232 234 bibi12d x = N x < y S x < S y N < y S N < S y
236 235 ralbidv x = N y 0 N x < y S x < S y y 0 N N < y S N < S y
237 236 rspcv N 0 N x 0 N y 0 N x < y S x < S y y 0 N N < y S N < S y
238 203 179 237 sylc φ y 0 N N < y S N < S y
239 238 r19.21bi φ y 0 N N < y S N < S y
240 231 239 mtbid φ y 0 N ¬ S N < S y
241 222 224 240 nltled φ y 0 N S y S N
242 241 3adant3 φ y 0 N S y = D S y S N
243 221 242 eqbrtrd φ y 0 N S y = D D S N
244 243 rexlimdv3a φ y 0 N S y = D D S N
245 219 244 mpd φ D S N
246 223 6 letri3d φ S N = D S N D D S N
247 209 245 246 mpbir2and φ S N = D
248 elfzoelz i 0 ..^ N i
249 248 zred i 0 ..^ N i
250 249 ltp1d i 0 ..^ N i < i + 1
251 250 adantl φ i 0 ..^ N i < i + 1
252 179 adantr φ i 0 ..^ N x 0 N y 0 N x < y S x < S y
253 elfzofz i 0 ..^ N i 0 N
254 253 adantl φ i 0 ..^ N i 0 N
255 fzofzp1 i 0 ..^ N i + 1 0 N
256 255 adantl φ i 0 ..^ N i + 1 0 N
257 breq1 x = i x < y i < y
258 fveq2 x = i S x = S i
259 258 breq1d x = i S x < S y S i < S y
260 257 259 bibi12d x = i x < y S x < S y i < y S i < S y
261 breq2 y = i + 1 i < y i < i + 1
262 fveq2 y = i + 1 S y = S i + 1
263 262 breq2d y = i + 1 S i < S y S i < S i + 1
264 261 263 bibi12d y = i + 1 i < y S i < S y i < i + 1 S i < S i + 1
265 260 264 rspc2v i 0 N i + 1 0 N x 0 N y 0 N x < y S x < S y i < i + 1 S i < S i + 1
266 254 256 265 syl2anc φ i 0 ..^ N x 0 N y 0 N x < y S x < S y i < i + 1 S i < S i + 1
267 252 266 mpd φ i 0 ..^ N i < i + 1 S i < S i + 1
268 251 267 mpbid φ i 0 ..^ N S i < S i + 1
269 268 ralrimiva φ i 0 ..^ N S i < S i + 1
270 201 247 269 jca31 φ S 0 = C S N = D i 0 ..^ N S i < S i + 1
271 8 fourierdlem2 N S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
272 99 271 syl φ S O N S 0 N S 0 = C S N = D i 0 ..^ N S i < S i + 1
273 120 270 272 mpbir2and φ S O N
274 99 273 108 jca31 φ N S O N S Isom < , < 0 N H