Metamath Proof Explorer


Theorem fourierdlem98

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem98.f φ F :
fourierdlem98.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem98.t T = B A
fourierdlem98.m φ M
fourierdlem98.q φ Q P M
fourierdlem98.fper φ x F x + T = F x
fourierdlem98.qcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem98.c φ C
fourierdlem98.d φ D C +∞
fourierdlem98.j φ J 0 ..^ C D y C D | k y + k T ran Q 1
fourierdlem98.v V = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
Assertion fourierdlem98 φ F V J V J + 1 : V J V J + 1 cn

Proof

Step Hyp Ref Expression
1 fourierdlem98.f φ F :
2 fourierdlem98.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
3 fourierdlem98.t T = B A
4 fourierdlem98.m φ M
5 fourierdlem98.q φ Q P M
6 fourierdlem98.fper φ x F x + T = F x
7 fourierdlem98.qcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
8 fourierdlem98.c φ C
9 fourierdlem98.d φ D C +∞
10 fourierdlem98.j φ J 0 ..^ C D y C D | k y + k T ran Q 1
11 fourierdlem98.v V = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
12 ax-resscn
13 12 a1i φ
14 1 13 fssd φ F :
15 eqid m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = C p m = D i 0 ..^ m p i < p i + 1
16 oveq1 z = y z + l T = y + l T
17 16 eleq1d z = y z + l T ran Q y + l T ran Q
18 17 rexbidv z = y l z + l T ran Q l y + l T ran Q
19 18 cbvrabv z C D | l z + l T ran Q = y C D | l y + l T ran Q
20 19 uneq2i C D z C D | l z + l T ran Q = C D y C D | l y + l T ran Q
21 20 eqcomi C D y C D | l y + l T ran Q = C D z C D | l z + l T ran Q
22 oveq1 k = l k T = l T
23 22 oveq2d k = l y + k T = y + l T
24 23 eleq1d k = l y + k T ran Q y + l T ran Q
25 24 cbvrexvw k y + k T ran Q l y + l T ran Q
26 25 a1i y C D k y + k T ran Q l y + l T ran Q
27 26 rabbiia y C D | k y + k T ran Q = y C D | l y + l T ran Q
28 27 uneq2i C D y C D | k y + k T ran Q = C D y C D | l y + l T ran Q
29 28 fveq2i C D y C D | k y + k T ran Q = C D y C D | l y + l T ran Q
30 29 oveq1i C D y C D | k y + k T ran Q 1 = C D y C D | l y + l T ran Q 1
31 oveq1 l = h l T = h T
32 31 oveq2d l = h y + l T = y + h T
33 32 eleq1d l = h y + l T ran Q y + h T ran Q
34 33 cbvrexvw l y + l T ran Q h y + h T ran Q
35 34 a1i y C D l y + l T ran Q h y + h T ran Q
36 35 rabbiia y C D | l y + l T ran Q = y C D | h y + h T ran Q
37 36 uneq2i C D y C D | l y + l T ran Q = C D y C D | h y + h T ran Q
38 isoeq5 C D y C D | l y + l T ran Q = C D y C D | h y + h T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
39 37 38 ax-mp g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
40 39 iotabii ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | h y + h T ran Q
41 isoeq1 f = g f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
42 41 cbviotavw ι f | f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q = ι g | g Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
43 40 42 11 3eqtr4ri V = ι f | f Isom < , < 0 C D y C D | k y + k T ran Q 1 C D y C D | l y + l T ran Q
44 id v = x v = x
45 oveq2 v = x B v = B x
46 45 oveq1d v = x B v T = B x T
47 46 fveq2d v = x B v T = B x T
48 47 oveq1d v = x B v T T = B x T T
49 44 48 oveq12d v = x v + B v T T = x + B x T T
50 49 cbvmptv v v + B v T T = x x + B x T T
51 eqeq1 u = z u = B z = B
52 id u = z u = z
53 51 52 ifbieq2d u = z if u = B A u = if z = B A z
54 53 cbvmptv u A B if u = B A u = z A B if z = B A z
55 eqid V J + 1 v v + B v T T V J + 1 = V J + 1 v v + B v T T V J + 1
56 eqid F u A B if u = B A u v v + B v T T V J v v + B v T T V J + 1 = F u A B if u = B A u v v + B v T T V J v v + B v T T V J + 1
57 eqid z u A B if u = B A u v v + B v T T V J + V J + 1 - v v + B v T T V J + 1 v v + B v T T V J + 1 + V J + 1 - v v + B v T T V J + 1 F u A B if u = B A u v v + B v T T V J v v + B v T T V J + 1 z V J + 1 v v + B v T T V J + 1 = z u A B if u = B A u v v + B v T T V J + V J + 1 - v v + B v T T V J + 1 v v + B v T T V J + 1 + V J + 1 - v v + B v T T V J + 1 F u A B if u = B A u v v + B v T T V J v v + B v T T V J + 1 z V J + 1 v v + B v T T V J + 1
58 fveq2 i = t Q i = Q t
59 58 breq1d i = t Q i u A B if u = B A u v v + B v T T x Q t u A B if u = B A u v v + B v T T x
60 59 cbvrabv i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x = t 0 ..^ M | Q t u A B if u = B A u v v + B v T T x
61 fveq2 w = x v v + B v T T w = v v + B v T T x
62 61 fveq2d w = x u A B if u = B A u v v + B v T T w = u A B if u = B A u v v + B v T T x
63 62 eqcomd w = x u A B if u = B A u v v + B v T T x = u A B if u = B A u v v + B v T T w
64 63 breq2d w = x Q t u A B if u = B A u v v + B v T T x Q t u A B if u = B A u v v + B v T T w
65 64 rabbidv w = x t 0 ..^ M | Q t u A B if u = B A u v v + B v T T x = t 0 ..^ M | Q t u A B if u = B A u v v + B v T T w
66 60 65 eqtr2id w = x t 0 ..^ M | Q t u A B if u = B A u v v + B v T T w = i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x
67 66 supeq1d w = x sup t 0 ..^ M | Q t u A B if u = B A u v v + B v T T w < = sup i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x <
68 67 cbvmptv w sup t 0 ..^ M | Q t u A B if u = B A u v v + B v T T w < = x sup i 0 ..^ M | Q i u A B if u = B A u v v + B v T T x <
69 2 3 4 5 14 6 7 8 9 15 21 30 43 50 54 10 55 56 57 68 fourierdlem90 φ F V J V J + 1 : V J V J + 1 cn