Metamath Proof Explorer


Theorem itgiccshift

Description: The integral of a function, F stays the same if its closed interval domain is shifted by T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgiccshift.a φ A
itgiccshift.b φ B
itgiccshift.aleb φ A B
itgiccshift.f φ F : A B cn
itgiccshift.t φ T +
itgiccshift.g G = x A + T B + T F x T
Assertion itgiccshift φ A + T B + T G x dx = A B F x dx

Proof

Step Hyp Ref Expression
1 itgiccshift.a φ A
2 itgiccshift.b φ B
3 itgiccshift.aleb φ A B
4 itgiccshift.f φ F : A B cn
5 itgiccshift.t φ T +
6 itgiccshift.g G = x A + T B + T F x T
7 5 rpred φ T
8 1 2 7 3 leadd1dd φ A + T B + T
9 8 ditgpos φ A + T B + T G x dx = A + T B + T G x dx
10 1 7 readdcld φ A + T
11 2 7 readdcld φ B + T
12 cncff F : A B cn F : A B
13 4 12 syl φ F : A B
14 13 adantr φ x A + T B + T F : A B
15 1 adantr φ x A + T B + T A
16 2 adantr φ x A + T B + T B
17 10 adantr φ x A + T B + T A + T
18 11 adantr φ x A + T B + T B + T
19 simpr φ x A + T B + T x A + T B + T
20 eliccre A + T B + T x A + T B + T x
21 17 18 19 20 syl3anc φ x A + T B + T x
22 7 adantr φ x A + T B + T T
23 21 22 resubcld φ x A + T B + T x T
24 1 recnd φ A
25 7 recnd φ T
26 24 25 pncand φ A + T - T = A
27 26 eqcomd φ A = A + T - T
28 27 adantr φ x A + T B + T A = A + T - T
29 elicc2 A + T B + T x A + T B + T x A + T x x B + T
30 17 18 29 syl2anc φ x A + T B + T x A + T B + T x A + T x x B + T
31 19 30 mpbid φ x A + T B + T x A + T x x B + T
32 31 simp2d φ x A + T B + T A + T x
33 17 21 22 32 lesub1dd φ x A + T B + T A + T - T x T
34 28 33 eqbrtrd φ x A + T B + T A x T
35 31 simp3d φ x A + T B + T x B + T
36 21 18 22 35 lesub1dd φ x A + T B + T x T B + T - T
37 2 recnd φ B
38 37 25 pncand φ B + T - T = B
39 38 adantr φ x A + T B + T B + T - T = B
40 36 39 breqtrd φ x A + T B + T x T B
41 15 16 23 34 40 eliccd φ x A + T B + T x T A B
42 14 41 ffvelrnd φ x A + T B + T F x T
43 42 6 fmptd φ G : A + T B + T
44 43 ffvelrnda φ x A + T B + T G x
45 10 11 44 itgioo φ A + T B + T G x dx = A + T B + T G x dx
46 9 45 eqtr2d φ A + T B + T G x dx = A + T B + T G x dx
47 eqid y y + T = y y + T
48 47 addccncf T y y + T : cn
49 25 48 syl φ y y + T : cn
50 1 2 iccssred φ A B
51 ax-resscn
52 50 51 sstrdi φ A B
53 10 11 iccssred φ A + T B + T
54 53 51 sstrdi φ A + T B + T
55 10 adantr φ y A B A + T
56 11 adantr φ y A B B + T
57 50 sselda φ y A B y
58 7 adantr φ y A B T
59 57 58 readdcld φ y A B y + T
60 1 adantr φ y A B A
61 simpr φ y A B y A B
62 2 adantr φ y A B B
63 elicc2 A B y A B y A y y B
64 60 62 63 syl2anc φ y A B y A B y A y y B
65 61 64 mpbid φ y A B y A y y B
66 65 simp2d φ y A B A y
67 60 57 58 66 leadd1dd φ y A B A + T y + T
68 65 simp3d φ y A B y B
69 57 62 58 68 leadd1dd φ y A B y + T B + T
70 55 56 59 67 69 eliccd φ y A B y + T A + T B + T
71 47 49 52 54 70 cncfmptssg φ y A B y + T : A B cn A + T B + T
72 fvoveq1 x = w F x T = F w T
73 72 cbvmptv x A + T B + T F x T = w A + T B + T F w T
74 1 2 7 iccshift φ A + T B + T = x | y A B x = y + T
75 74 mpteq1d φ w A + T B + T F w T = w x | y A B x = y + T F w T
76 73 75 syl5eq φ x A + T B + T F x T = w x | y A B x = y + T F w T
77 6 76 syl5eq φ G = w x | y A B x = y + T F w T
78 eqeq1 w = x w = z + T x = z + T
79 78 rexbidv w = x z A B w = z + T z A B x = z + T
80 oveq1 z = y z + T = y + T
81 80 eqeq2d z = y x = z + T x = y + T
82 81 cbvrexvw z A B x = z + T y A B x = y + T
83 79 82 bitrdi w = x z A B w = z + T y A B x = y + T
84 83 cbvrabv w | z A B w = z + T = x | y A B x = y + T
85 84 eqcomi x | y A B x = y + T = w | z A B w = z + T
86 eqid w x | y A B x = y + T F w T = w x | y A B x = y + T F w T
87 52 25 85 4 86 cncfshift φ w x | y A B x = y + T F w T : x | y A B x = y + T cn
88 77 87 eqeltrd φ G : x | y A B x = y + T cn
89 43 feqmptd φ G = x A + T B + T G x
90 74 eqcomd φ x | y A B x = y + T = A + T B + T
91 90 oveq1d φ x | y A B x = y + T cn = A + T B + T cn
92 88 89 91 3eltr3d φ x A + T B + T G x : A + T B + T cn
93 ioosscn A B
94 93 a1i φ A B
95 1cnd φ 1
96 ssid
97 96 a1i φ
98 94 95 97 constcncfg φ y A B 1 : A B cn
99 fconstmpt A B × 1 = y A B 1
100 ioombl A B dom vol
101 100 a1i φ A B dom vol
102 ioovolcl A B vol A B
103 1 2 102 syl2anc φ vol A B
104 iblconst A B dom vol vol A B 1 A B × 1 𝐿 1
105 101 103 95 104 syl3anc φ A B × 1 𝐿 1
106 99 105 eqeltrrid φ y A B 1 𝐿 1
107 98 106 elind φ y A B 1 A B cn 𝐿 1
108 50 resmptd φ y y + T A B = y A B y + T
109 108 eqcomd φ y A B y + T = y y + T A B
110 109 oveq2d φ dy A B y + T d y = D y y + T A B
111 51 a1i φ
112 111 sselda φ y y
113 25 adantr φ y T
114 112 113 addcld φ y y + T
115 114 fmpttd φ y y + T :
116 ssid
117 116 a1i φ
118 eqid TopOpen fld = TopOpen fld
119 118 tgioo2 topGen ran . = TopOpen fld 𝑡
120 118 119 dvres y y + T : A B D y y + T A B = dy y + T d y int topGen ran . A B
121 111 115 117 50 120 syl22anc φ D y y + T A B = dy y + T d y int topGen ran . A B
122 110 121 eqtrd φ dy A B y + T d y = dy y + T d y int topGen ran . A B
123 iccntr A B int topGen ran . A B = A B
124 1 2 123 syl2anc φ int topGen ran . A B = A B
125 124 reseq2d φ dy y + T d y int topGen ran . A B = dy y + T d y A B
126 reelprrecn
127 126 a1i φ
128 1cnd φ y 1
129 127 dvmptid φ dy y d y = y 1
130 0cnd φ y 0
131 127 25 dvmptc φ dy T d y = y 0
132 127 112 128 129 113 130 131 dvmptadd φ dy y + T d y = y 1 + 0
133 132 reseq1d φ dy y + T d y A B = y 1 + 0 A B
134 ioossre A B
135 134 a1i φ A B
136 135 resmptd φ y 1 + 0 A B = y A B 1 + 0
137 1p0e1 1 + 0 = 1
138 137 mpteq2i y A B 1 + 0 = y A B 1
139 138 a1i φ y A B 1 + 0 = y A B 1
140 133 136 139 3eqtrd φ dy y + T d y A B = y A B 1
141 122 125 140 3eqtrd φ dy A B y + T d y = y A B 1
142 fveq2 x = y + T G x = G y + T
143 oveq1 y = A y + T = A + T
144 oveq1 y = B y + T = B + T
145 1 2 3 71 92 107 141 142 143 144 10 11 itgsubsticc φ A + T B + T G x dx = A B G y + T 1 dy
146 3 ditgpos φ A B G y + T 1 dy = A B G y + T 1 dy
147 43 adantr φ y A B G : A + T B + T
148 147 70 ffvelrnd φ y A B G y + T
149 1cnd φ y A B 1
150 148 149 mulcld φ y A B G y + T 1
151 1 2 150 itgioo φ A B G y + T 1 dy = A B G y + T 1 dy
152 fvoveq1 y = x G y + T = G x + T
153 152 oveq1d y = x G y + T 1 = G x + T 1
154 153 cbvitgv A B G y + T 1 dy = A B G x + T 1 dx
155 43 adantr φ x A B G : A + T B + T
156 10 adantr φ x A B A + T
157 11 adantr φ x A B B + T
158 50 sselda φ x A B x
159 7 adantr φ x A B T
160 158 159 readdcld φ x A B x + T
161 1 adantr φ x A B A
162 1 rexrd φ A *
163 162 adantr φ x A B A *
164 2 rexrd φ B *
165 164 adantr φ x A B B *
166 simpr φ x A B x A B
167 iccgelb A * B * x A B A x
168 163 165 166 167 syl3anc φ x A B A x
169 161 158 159 168 leadd1dd φ x A B A + T x + T
170 2 adantr φ x A B B
171 iccleub A * B * x A B x B
172 163 165 166 171 syl3anc φ x A B x B
173 158 170 159 172 leadd1dd φ x A B x + T B + T
174 156 157 160 169 173 eliccd φ x A B x + T A + T B + T
175 155 174 ffvelrnd φ x A B G x + T
176 175 mulid1d φ x A B G x + T 1 = G x + T
177 6 73 eqtri G = w A + T B + T F w T
178 177 a1i φ x A B G = w A + T B + T F w T
179 fvoveq1 w = x + T F w T = F x + T - T
180 158 recnd φ x A B x
181 25 adantr φ x A B T
182 180 181 pncand φ x A B x + T - T = x
183 182 fveq2d φ x A B F x + T - T = F x
184 179 183 sylan9eqr φ x A B w = x + T F w T = F x
185 13 ffvelrnda φ x A B F x
186 178 184 174 185 fvmptd φ x A B G x + T = F x
187 176 186 eqtrd φ x A B G x + T 1 = F x
188 187 itgeq2dv φ A B G x + T 1 dx = A B F x dx
189 154 188 syl5eq φ A B G y + T 1 dy = A B F x dx
190 146 151 189 3eqtrd φ A B G y + T 1 dy = A B F x dx
191 46 145 190 3eqtrd φ A + T B + T G x dx = A B F x dx