# 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 ${⊢}{\phi }\to {A}\in ℝ$
itgiccshift.b ${⊢}{\phi }\to {B}\in ℝ$
itgiccshift.aleb ${⊢}{\phi }\to {A}\le {B}$
itgiccshift.f ${⊢}{\phi }\to {F}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
itgiccshift.t ${⊢}{\phi }\to {T}\in {ℝ}^{+}$
itgiccshift.g ${⊢}{G}=\left({x}\in \left[{A}+{T},{B}+{T}\right]⟼{F}\left({x}-{T}\right)\right)$
Assertion itgiccshift ${⊢}{\phi }\to {\int }_{\left[{A}+{T},{B}+{T}\right]}{G}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}$

### Proof

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