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 syl6bb 
 |-  ( 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 )