Metamath Proof Explorer


Theorem itgperiod

Description: The integral of a periodic function, with period T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgperiod.a
|- ( ph -> A e. RR )
itgperiod.b
|- ( ph -> B e. RR )
itgperiod.aleb
|- ( ph -> A <_ B )
itgperiod.t
|- ( ph -> T e. RR+ )
itgperiod.f
|- ( ph -> F : RR --> CC )
itgperiod.fper
|- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
itgperiod.fcn
|- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
Assertion itgperiod
|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step Hyp Ref Expression
1 itgperiod.a
 |-  ( ph -> A e. RR )
2 itgperiod.b
 |-  ( ph -> B e. RR )
3 itgperiod.aleb
 |-  ( ph -> A <_ B )
4 itgperiod.t
 |-  ( ph -> T e. RR+ )
5 itgperiod.f
 |-  ( ph -> F : RR --> CC )
6 itgperiod.fper
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7 itgperiod.fcn
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
8 4 rpred
 |-  ( ph -> T e. RR )
9 1 2 8 3 leadd1dd
 |-  ( ph -> ( A + T ) <_ ( B + T ) )
10 9 ditgpos
 |-  ( ph -> S_ [ ( A + T ) -> ( B + T ) ] ( F ` x ) _d x = S. ( ( A + T ) (,) ( B + T ) ) ( F ` x ) _d x )
11 1 8 readdcld
 |-  ( ph -> ( A + T ) e. RR )
12 2 8 readdcld
 |-  ( ph -> ( B + T ) e. RR )
13 5 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> F : RR --> CC )
14 11 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
15 12 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
16 simpr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
17 eliccre
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
18 14 15 16 17 syl3anc
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
19 13 18 ffvelrnd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` x ) e. CC )
20 11 12 19 itgioo
 |-  ( ph -> S. ( ( A + T ) (,) ( B + T ) ) ( F ` x ) _d x = S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x )
21 10 20 eqtr2d
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S_ [ ( A + T ) -> ( B + T ) ] ( F ` x ) _d x )
22 eqid
 |-  ( y e. CC |-> ( y + T ) ) = ( y e. CC |-> ( y + T ) )
23 8 recnd
 |-  ( ph -> T e. CC )
24 22 addccncf
 |-  ( T e. CC -> ( y e. CC |-> ( y + T ) ) e. ( CC -cn-> CC ) )
25 23 24 syl
 |-  ( ph -> ( y e. CC |-> ( y + T ) ) e. ( CC -cn-> CC ) )
26 1 2 iccssred
 |-  ( ph -> ( A [,] B ) C_ RR )
27 ax-resscn
 |-  RR C_ CC
28 26 27 sstrdi
 |-  ( ph -> ( A [,] B ) C_ CC )
29 11 12 iccssred
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) C_ RR )
30 29 27 sstrdi
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) C_ CC )
31 11 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( A + T ) e. RR )
32 12 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( B + T ) e. RR )
33 26 sselda
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR )
34 8 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> T e. RR )
35 33 34 readdcld
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) e. RR )
36 1 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> A e. RR )
37 simpr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
38 2 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> B e. RR )
39 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
40 36 38 39 syl2anc
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
41 37 40 mpbid
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
42 41 simp2d
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> A <_ y )
43 36 33 34 42 leadd1dd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( A + T ) <_ ( y + T ) )
44 41 simp3d
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> y <_ B )
45 33 38 34 44 leadd1dd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) <_ ( B + T ) )
46 31 32 35 43 45 eliccd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) e. ( ( A + T ) [,] ( B + T ) ) )
47 22 25 28 30 46 cncfmptssg
 |-  ( ph -> ( y e. ( A [,] B ) |-> ( y + T ) ) e. ( ( A [,] B ) -cn-> ( ( A + T ) [,] ( B + T ) ) ) )
48 eqeq1
 |-  ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
49 48 rexbidv
 |-  ( w = x -> ( E. z e. ( A [,] B ) w = ( z + T ) <-> E. z e. ( A [,] B ) x = ( z + T ) ) )
50 oveq1
 |-  ( z = y -> ( z + T ) = ( y + T ) )
51 50 eqeq2d
 |-  ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
52 51 cbvrexvw
 |-  ( E. z e. ( A [,] B ) x = ( z + T ) <-> E. y e. ( A [,] B ) x = ( y + T ) )
53 49 52 bitrdi
 |-  ( w = x -> ( E. z e. ( A [,] B ) w = ( z + T ) <-> E. y e. ( A [,] B ) x = ( y + T ) ) )
54 53 cbvrabv
 |-  { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) }
55 5 ffdmd
 |-  ( ph -> F : dom F --> CC )
56 simp3
 |-  ( ( ph /\ z e. ( A [,] B ) /\ w = ( z + T ) ) -> w = ( z + T ) )
57 26 sselda
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z e. RR )
58 8 adantr
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> T e. RR )
59 57 58 readdcld
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) e. RR )
60 59 3adant3
 |-  ( ( ph /\ z e. ( A [,] B ) /\ w = ( z + T ) ) -> ( z + T ) e. RR )
61 56 60 eqeltrd
 |-  ( ( ph /\ z e. ( A [,] B ) /\ w = ( z + T ) ) -> w e. RR )
62 61 rexlimdv3a
 |-  ( ph -> ( E. z e. ( A [,] B ) w = ( z + T ) -> w e. RR ) )
63 62 ralrimivw
 |-  ( ph -> A. w e. CC ( E. z e. ( A [,] B ) w = ( z + T ) -> w e. RR ) )
64 rabss
 |-  ( { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } C_ RR <-> A. w e. CC ( E. z e. ( A [,] B ) w = ( z + T ) -> w e. RR ) )
65 63 64 sylibr
 |-  ( ph -> { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } C_ RR )
66 5 fdmd
 |-  ( ph -> dom F = RR )
67 65 66 sseqtrrd
 |-  ( ph -> { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } C_ dom F )
68 28 8 54 55 67 6 7 cncfperiod
 |-  ( ph -> ( F |` { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) e. ( { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } -cn-> CC ) )
69 49 elrab
 |-  ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
70 simprr
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
71 nfv
 |-  F/ z ph
72 nfv
 |-  F/ z x e. CC
73 nfre1
 |-  F/ z E. z e. ( A [,] B ) x = ( z + T )
74 72 73 nfan
 |-  F/ z ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) )
75 71 74 nfan
 |-  F/ z ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
76 nfv
 |-  F/ z x e. ( ( A + T ) [,] ( B + T ) )
77 simp3
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> x = ( z + T ) )
78 1 adantr
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> A e. RR )
79 simpr
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
80 2 adantr
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> B e. RR )
81 elicc2
 |-  ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
82 78 80 81 syl2anc
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
83 79 82 mpbid
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. RR /\ A <_ z /\ z <_ B ) )
84 83 simp2d
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> A <_ z )
85 78 57 58 84 leadd1dd
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( A + T ) <_ ( z + T ) )
86 83 simp3d
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> z <_ B )
87 57 80 58 86 leadd1dd
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) <_ ( B + T ) )
88 59 85 87 3jca
 |-  ( ( ph /\ z e. ( A [,] B ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
89 88 3adant3
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
90 11 3ad2ant1
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( A + T ) e. RR )
91 12 3ad2ant1
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( B + T ) e. RR )
92 elicc2
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) ) )
93 90 91 92 syl2anc
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) ) )
94 89 93 mpbird
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) )
95 77 94 eqeltrd
 |-  ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
96 95 3exp
 |-  ( ph -> ( z e. ( A [,] B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) ) )
97 96 adantr
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> ( z e. ( A [,] B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) ) )
98 75 76 97 rexlimd
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> ( E. z e. ( A [,] B ) x = ( z + T ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) )
99 70 98 mpd
 |-  ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
100 69 99 sylan2b
 |-  ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
101 18 recnd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
102 1 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
103 2 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> B e. RR )
104 8 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. RR )
105 18 104 resubcld
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) e. RR )
106 1 recnd
 |-  ( ph -> A e. CC )
107 106 23 pncand
 |-  ( ph -> ( ( A + T ) - T ) = A )
108 107 eqcomd
 |-  ( ph -> A = ( ( A + T ) - T ) )
109 108 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A = ( ( A + T ) - T ) )
110 elicc2
 |-  ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
111 14 15 110 syl2anc
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
112 16 111 mpbid
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) )
113 112 simp2d
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
114 14 18 104 113 lesub1dd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) - T ) <_ ( x - T ) )
115 109 114 eqbrtrd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x - T ) )
116 112 simp3d
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
117 18 15 104 116 lesub1dd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ ( ( B + T ) - T ) )
118 2 recnd
 |-  ( ph -> B e. CC )
119 118 23 pncand
 |-  ( ph -> ( ( B + T ) - T ) = B )
120 119 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
121 117 120 breqtrd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ B )
122 102 103 105 115 121 eliccd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
123 23 adantr
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
124 101 123 npcand
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
125 124 eqcomd
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x = ( ( x - T ) + T ) )
126 oveq1
 |-  ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
127 126 rspceeqv
 |-  ( ( ( x - T ) e. ( A [,] B ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
128 122 125 127 syl2anc
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
129 101 128 69 sylanbrc
 |-  ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
130 100 129 impbida
 |-  ( ph -> ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> x e. ( ( A + T ) [,] ( B + T ) ) ) )
131 130 eqrdv
 |-  ( ph -> { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = ( ( A + T ) [,] ( B + T ) ) )
132 131 reseq2d
 |-  ( ph -> ( F |` { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) = ( F |` ( ( A + T ) [,] ( B + T ) ) ) )
133 131 67 eqsstrrd
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) C_ dom F )
134 55 133 feqresmpt
 |-  ( ph -> ( F |` ( ( A + T ) [,] ( B + T ) ) ) = ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` x ) ) )
135 132 134 eqtr2d
 |-  ( ph -> ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` x ) ) = ( F |` { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) )
136 1 2 8 iccshift
 |-  ( ph -> ( ( A + T ) [,] ( B + T ) ) = { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
137 136 oveq1d
 |-  ( ph -> ( ( ( A + T ) [,] ( B + T ) ) -cn-> CC ) = ( { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } -cn-> CC ) )
138 68 135 137 3eltr4d
 |-  ( ph -> ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` x ) ) e. ( ( ( A + T ) [,] ( B + T ) ) -cn-> CC ) )
139 ioosscn
 |-  ( A (,) B ) C_ CC
140 139 a1i
 |-  ( ph -> ( A (,) B ) C_ CC )
141 1cnd
 |-  ( ph -> 1 e. CC )
142 ssid
 |-  CC C_ CC
143 142 a1i
 |-  ( ph -> CC C_ CC )
144 140 141 143 constcncfg
 |-  ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
145 fconstmpt
 |-  ( ( A (,) B ) X. { 1 } ) = ( y e. ( A (,) B ) |-> 1 )
146 ioombl
 |-  ( A (,) B ) e. dom vol
147 146 a1i
 |-  ( ph -> ( A (,) B ) e. dom vol )
148 ioovolcl
 |-  ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
149 1 2 148 syl2anc
 |-  ( ph -> ( vol ` ( A (,) B ) ) e. RR )
150 iblconst
 |-  ( ( ( A (,) B ) e. dom vol /\ ( vol ` ( A (,) B ) ) e. RR /\ 1 e. CC ) -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
151 147 149 141 150 syl3anc
 |-  ( ph -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
152 145 151 eqeltrrid
 |-  ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. L^1 )
153 144 152 elind
 |-  ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. ( ( ( A (,) B ) -cn-> CC ) i^i L^1 ) )
154 26 resmptd
 |-  ( ph -> ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) = ( y e. ( A [,] B ) |-> ( y + T ) ) )
155 154 eqcomd
 |-  ( ph -> ( y e. ( A [,] B ) |-> ( y + T ) ) = ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) )
156 155 oveq2d
 |-  ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( RR _D ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) ) )
157 27 a1i
 |-  ( ph -> RR C_ CC )
158 157 sselda
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
159 23 adantr
 |-  ( ( ph /\ y e. RR ) -> T e. CC )
160 158 159 addcld
 |-  ( ( ph /\ y e. RR ) -> ( y + T ) e. CC )
161 160 fmpttd
 |-  ( ph -> ( y e. RR |-> ( y + T ) ) : RR --> CC )
162 ssid
 |-  RR C_ RR
163 162 a1i
 |-  ( ph -> RR C_ RR )
164 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
165 164 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
166 164 165 dvres
 |-  ( ( ( RR C_ CC /\ ( y e. RR |-> ( y + T ) ) : RR --> CC ) /\ ( RR C_ RR /\ ( A [,] B ) C_ RR ) ) -> ( RR _D ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
167 157 161 163 26 166 syl22anc
 |-  ( ph -> ( RR _D ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
168 156 167 eqtrd
 |-  ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
169 iccntr
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
170 1 2 169 syl2anc
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
171 170 reseq2d
 |-  ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) )
172 reelprrecn
 |-  RR e. { RR , CC }
173 172 a1i
 |-  ( ph -> RR e. { RR , CC } )
174 1cnd
 |-  ( ( ph /\ y e. RR ) -> 1 e. CC )
175 173 dvmptid
 |-  ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
176 0cnd
 |-  ( ( ph /\ y e. RR ) -> 0 e. CC )
177 173 23 dvmptc
 |-  ( ph -> ( RR _D ( y e. RR |-> T ) ) = ( y e. RR |-> 0 ) )
178 173 158 174 175 159 176 177 dvmptadd
 |-  ( ph -> ( RR _D ( y e. RR |-> ( y + T ) ) ) = ( y e. RR |-> ( 1 + 0 ) ) )
179 178 reseq1d
 |-  ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) = ( ( y e. RR |-> ( 1 + 0 ) ) |` ( A (,) B ) ) )
180 ioossre
 |-  ( A (,) B ) C_ RR
181 180 a1i
 |-  ( ph -> ( A (,) B ) C_ RR )
182 181 resmptd
 |-  ( ph -> ( ( y e. RR |-> ( 1 + 0 ) ) |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) )
183 1p0e1
 |-  ( 1 + 0 ) = 1
184 183 mpteq2i
 |-  ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) = ( y e. ( A (,) B ) |-> 1 )
185 184 a1i
 |-  ( ph -> ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) = ( y e. ( A (,) B ) |-> 1 ) )
186 179 182 185 3eqtrd
 |-  ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> 1 ) )
187 168 171 186 3eqtrd
 |-  ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( y e. ( A (,) B ) |-> 1 ) )
188 fveq2
 |-  ( x = ( y + T ) -> ( F ` x ) = ( F ` ( y + T ) ) )
189 oveq1
 |-  ( y = A -> ( y + T ) = ( A + T ) )
190 oveq1
 |-  ( y = B -> ( y + T ) = ( B + T ) )
191 1 2 3 47 138 153 187 188 189 190 11 12 itgsubsticc
 |-  ( ph -> S_ [ ( A + T ) -> ( B + T ) ] ( F ` x ) _d x = S_ [ A -> B ] ( ( F ` ( y + T ) ) x. 1 ) _d y )
192 3 ditgpos
 |-  ( ph -> S_ [ A -> B ] ( ( F ` ( y + T ) ) x. 1 ) _d y = S. ( A (,) B ) ( ( F ` ( y + T ) ) x. 1 ) _d y )
193 5 adantr
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> F : RR --> CC )
194 193 35 ffvelrnd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( F ` ( y + T ) ) e. CC )
195 1cnd
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> 1 e. CC )
196 194 195 mulcld
 |-  ( ( ph /\ y e. ( A [,] B ) ) -> ( ( F ` ( y + T ) ) x. 1 ) e. CC )
197 1 2 196 itgioo
 |-  ( ph -> S. ( A (,) B ) ( ( F ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( ( F ` ( y + T ) ) x. 1 ) _d y )
198 fvoveq1
 |-  ( y = x -> ( F ` ( y + T ) ) = ( F ` ( x + T ) ) )
199 198 oveq1d
 |-  ( y = x -> ( ( F ` ( y + T ) ) x. 1 ) = ( ( F ` ( x + T ) ) x. 1 ) )
200 199 cbvitgv
 |-  S. ( A [,] B ) ( ( F ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( ( F ` ( x + T ) ) x. 1 ) _d x
201 5 adantr
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> F : RR --> CC )
202 26 sselda
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
203 8 adantr
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> T e. RR )
204 202 203 readdcld
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x + T ) e. RR )
205 201 204 ffvelrnd
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( x + T ) ) e. CC )
206 205 mulid1d
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( F ` ( x + T ) ) x. 1 ) = ( F ` ( x + T ) ) )
207 206 6 eqtrd
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( F ` ( x + T ) ) x. 1 ) = ( F ` x ) )
208 207 itgeq2dv
 |-  ( ph -> S. ( A [,] B ) ( ( F ` ( x + T ) ) x. 1 ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
209 200 208 syl5eq
 |-  ( ph -> S. ( A [,] B ) ( ( F ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( F ` x ) _d x )
210 192 197 209 3eqtrd
 |-  ( ph -> S_ [ A -> B ] ( ( F ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( F ` x ) _d x )
211 21 191 210 3eqtrd
 |-  ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )