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
|- ( ph -> A e. RR )
itgiccshift.b
|- ( ph -> B e. RR )
itgiccshift.aleb
|- ( ph -> A <_ B )
itgiccshift.f
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
itgiccshift.t
|- ( ph -> T e. RR+ )
itgiccshift.g
|- G = ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( x - T ) ) )
Assertion itgiccshift
|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

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