Metamath Proof Explorer


Theorem fourierdlem109

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem109.a φ A
fourierdlem109.b φ B
fourierdlem109.t T = B A
fourierdlem109.x φ X
fourierdlem109.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
fourierdlem109.m φ M
fourierdlem109.q φ Q P M
fourierdlem109.f φ F :
fourierdlem109.fper φ x F x + T = F x
fourierdlem109.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem109.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
fourierdlem109.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
fourierdlem109.o O = m p 0 m | p 0 = A X p m = B X i 0 ..^ m p i < p i + 1
fourierdlem109.h H = A X B X x A X B X | k x + k T ran Q
fourierdlem109.n N = H 1
fourierdlem109.16 S = ι f | f Isom < , < 0 N H
fourierdlem109.17 E = x x + B x T T
fourierdlem109.18 J = y A B if y = B A y
fourierdlem109.19 I = x sup j 0 ..^ M | Q j J E x <
Assertion fourierdlem109 φ A X B X F x dx = A B F x dx

Proof

Step Hyp Ref Expression
1 fourierdlem109.a φ A
2 fourierdlem109.b φ B
3 fourierdlem109.t T = B A
4 fourierdlem109.x φ X
5 fourierdlem109.p P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
6 fourierdlem109.m φ M
7 fourierdlem109.q φ Q P M
8 fourierdlem109.f φ F :
9 fourierdlem109.fper φ x F x + T = F x
10 fourierdlem109.fcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
11 fourierdlem109.r φ i 0 ..^ M R F Q i Q i + 1 lim Q i
12 fourierdlem109.l φ i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
13 fourierdlem109.o O = m p 0 m | p 0 = A X p m = B X i 0 ..^ m p i < p i + 1
14 fourierdlem109.h H = A X B X x A X B X | k x + k T ran Q
15 fourierdlem109.n N = H 1
16 fourierdlem109.16 S = ι f | f Isom < , < 0 N H
17 fourierdlem109.17 E = x x + B x T T
18 fourierdlem109.18 J = y A B if y = B A y
19 fourierdlem109.19 I = x sup j 0 ..^ M | Q j J E x <
20 1 adantr φ 0 < X A
21 2 adantr φ 0 < X B
22 4 adantr φ 0 < X X
23 simpr φ 0 < X 0 < X
24 22 23 elrpd φ 0 < X X +
25 6 adantr φ 0 < X M
26 7 adantr φ 0 < X Q P M
27 8 adantr φ 0 < X F :
28 9 adantlr φ 0 < X x F x + T = F x
29 10 adantlr φ 0 < X i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
30 11 adantlr φ 0 < X i 0 ..^ M R F Q i Q i + 1 lim Q i
31 12 adantlr φ 0 < X i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
32 20 21 3 24 5 25 26 27 28 29 30 31 fourierdlem108 φ 0 < X A X B X F x dx = A B F x dx
33 oveq2 X = 0 A X = A 0
34 1 recnd φ A
35 34 subid1d φ A 0 = A
36 33 35 sylan9eqr φ X = 0 A X = A
37 oveq2 X = 0 B X = B 0
38 2 recnd φ B
39 38 subid1d φ B 0 = B
40 37 39 sylan9eqr φ X = 0 B X = B
41 36 40 oveq12d φ X = 0 A X B X = A B
42 41 itgeq1d φ X = 0 A X B X F x dx = A B F x dx
43 42 adantlr φ ¬ 0 < X X = 0 A X B X F x dx = A B F x dx
44 simpll φ ¬ 0 < X ¬ X = 0 φ
45 44 4 syl φ ¬ 0 < X ¬ X = 0 X
46 0red φ ¬ 0 < X ¬ X = 0 0
47 simpr φ ¬ 0 < X ¬ X = 0 ¬ X = 0
48 47 neqned φ ¬ 0 < X ¬ X = 0 X 0
49 simplr φ ¬ 0 < X ¬ X = 0 ¬ 0 < X
50 45 46 48 49 lttri5d φ ¬ 0 < X ¬ X = 0 X < 0
51 4 recnd φ X
52 34 51 subcld φ A X
53 52 51 subnegd φ A - X - X = A - X + X
54 34 51 npcand φ A - X + X = A
55 53 54 eqtrd φ A - X - X = A
56 38 51 subcld φ B X
57 56 51 subnegd φ B - X - X = B - X + X
58 38 51 npcand φ B - X + X = B
59 57 58 eqtrd φ B - X - X = B
60 55 59 oveq12d φ A - X - X B - X - X = A B
61 60 eqcomd φ A B = A - X - X B - X - X
62 61 itgeq1d φ A B F x dx = A - X - X B - X - X F x dx
63 62 adantr φ X < 0 A B F x dx = A - X - X B - X - X F x dx
64 1 4 resubcld φ A X
65 64 adantr φ X < 0 A X
66 2 4 resubcld φ B X
67 66 adantr φ X < 0 B X
68 eqid B - X - A X = B - X - A X
69 4 renegcld φ X
70 69 adantr φ X < 0 X
71 4 lt0neg1d φ X < 0 0 < X
72 71 biimpa φ X < 0 0 < X
73 70 72 elrpd φ X < 0 X +
74 fveq2 i = j p i = p j
75 oveq1 i = j i + 1 = j + 1
76 75 fveq2d i = j p i + 1 = p j + 1
77 74 76 breq12d i = j p i < p i + 1 p j < p j + 1
78 77 cbvralvw i 0 ..^ m p i < p i + 1 j 0 ..^ m p j < p j + 1
79 78 anbi2i p 0 = A X p m = B X i 0 ..^ m p i < p i + 1 p 0 = A X p m = B X j 0 ..^ m p j < p j + 1
80 79 a1i p 0 m p 0 = A X p m = B X i 0 ..^ m p i < p i + 1 p 0 = A X p m = B X j 0 ..^ m p j < p j + 1
81 80 rabbiia p 0 m | p 0 = A X p m = B X i 0 ..^ m p i < p i + 1 = p 0 m | p 0 = A X p m = B X j 0 ..^ m p j < p j + 1
82 81 mpteq2i m p 0 m | p 0 = A X p m = B X i 0 ..^ m p i < p i + 1 = m p 0 m | p 0 = A X p m = B X j 0 ..^ m p j < p j + 1
83 13 82 eqtri O = m p 0 m | p 0 = A X p m = B X j 0 ..^ m p j < p j + 1
84 5 6 7 fourierdlem11 φ A B A < B
85 84 simp3d φ A < B
86 1 2 4 85 ltsub1dd φ A X < B X
87 3 5 6 7 64 66 86 13 14 15 16 fourierdlem54 φ N S O N S Isom < , < 0 N H
88 87 simpld φ N S O N
89 88 simpld φ N
90 89 adantr φ X < 0 N
91 88 simprd φ S O N
92 91 adantr φ X < 0 S O N
93 8 adantr φ X < 0 F :
94 38 34 51 nnncan2d φ B - X - A X = B A
95 94 3 eqtr4di φ B - X - A X = T
96 95 oveq2d φ x + B X - A X = x + T
97 96 adantr φ x x + B X - A X = x + T
98 97 fveq2d φ x F x + B X - A X = F x + T
99 98 9 eqtrd φ x F x + B X - A X = F x
100 99 adantlr φ X < 0 x F x + B X - A X = F x
101 6 adantr φ j 0 ..^ N M
102 7 adantr φ j 0 ..^ N Q P M
103 8 adantr φ j 0 ..^ N F :
104 9 adantlr φ j 0 ..^ N x F x + T = F x
105 10 adantlr φ j 0 ..^ N i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
106 64 adantr φ j 0 ..^ N A X
107 64 rexrd φ A X *
108 pnfxr +∞ *
109 108 a1i φ +∞ *
110 66 ltpnfd φ B X < +∞
111 107 109 66 86 110 eliood φ B X A X +∞
112 111 adantr φ j 0 ..^ N B X A X +∞
113 oveq1 x = y x + k T = y + k T
114 113 eleq1d x = y x + k T ran Q y + k T ran Q
115 114 rexbidv x = y k x + k T ran Q k y + k T ran Q
116 115 cbvrabv x A X B X | k x + k T ran Q = y A X B X | k y + k T ran Q
117 116 uneq2i A X B X x A X B X | k x + k T ran Q = A X B X y A X B X | k y + k T ran Q
118 14 117 eqtri H = A X B X y A X B X | k y + k T ran Q
119 simpr φ j 0 ..^ N j 0 ..^ N
120 eqid S j + 1 E S j + 1 = S j + 1 E S j + 1
121 eqid F J E S j E S j + 1 = F J E S j E S j + 1
122 eqid y J E S j + S j + 1 - E S j + 1 E S j + 1 + S j + 1 - E S j + 1 F J E S j E S j + 1 y S j + 1 E S j + 1 = y J E S j + S j + 1 - E S j + 1 E S j + 1 + S j + 1 - E S j + 1 F J E S j E S j + 1 y S j + 1 E S j + 1
123 fveq2 j = i Q j = Q i
124 123 breq1d j = i Q j J E x Q i J E x
125 124 cbvrabv j 0 ..^ M | Q j J E x = i 0 ..^ M | Q i J E x
126 125 supeq1i sup j 0 ..^ M | Q j J E x < = sup i 0 ..^ M | Q i J E x <
127 126 mpteq2i x sup j 0 ..^ M | Q j J E x < = x sup i 0 ..^ M | Q i J E x <
128 19 127 eqtri I = x sup i 0 ..^ M | Q i J E x <
129 5 3 101 102 103 104 105 106 112 13 118 15 16 17 18 119 120 121 122 128 fourierdlem90 φ j 0 ..^ N F S j S j + 1 : S j S j + 1 cn
130 129 adantlr φ X < 0 j 0 ..^ N F S j S j + 1 : S j S j + 1 cn
131 11 adantlr φ j 0 ..^ N i 0 ..^ M R F Q i Q i + 1 lim Q i
132 eqid i 0 ..^ M R = i 0 ..^ M R
133 5 3 101 102 103 104 105 131 106 112 13 118 15 16 17 18 119 120 128 132 fourierdlem89 φ j 0 ..^ N if J E S j = Q I S j i 0 ..^ M R I S j F J E S j F S j S j + 1 lim S j
134 133 adantlr φ X < 0 j 0 ..^ N if J E S j = Q I S j i 0 ..^ M R I S j F J E S j F S j S j + 1 lim S j
135 12 adantlr φ j 0 ..^ N i 0 ..^ M L F Q i Q i + 1 lim Q i + 1
136 eqid i 0 ..^ M L = i 0 ..^ M L
137 5 3 101 102 103 104 105 135 106 112 13 118 15 16 17 18 119 120 128 136 fourierdlem91 φ j 0 ..^ N if E S j + 1 = Q I S j + 1 i 0 ..^ M L I S j F E S j + 1 F S j S j + 1 lim S j + 1
138 137 adantlr φ X < 0 j 0 ..^ N if E S j + 1 = Q I S j + 1 i 0 ..^ M L I S j F E S j + 1 F S j S j + 1 lim S j + 1
139 65 67 68 73 83 90 92 93 100 130 134 138 fourierdlem108 φ X < 0 A - X - X B - X - X F x dx = A X B X F x dx
140 63 139 eqtr2d φ X < 0 A X B X F x dx = A B F x dx
141 44 50 140 syl2anc φ ¬ 0 < X ¬ X = 0 A X B X F x dx = A B F x dx
142 43 141 pm2.61dan φ ¬ 0 < X A X B X F x dx = A B F x dx
143 32 142 pm2.61dan φ A X B X F x dx = A B F x dx