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