Theorem itgiccshift 31621

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
itgiccshift	|- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Distinct variable groups:   x, A   x, B   x, F   x, G   x, T   ph, x

Proof of Theorem itgiccshift

Dummy variables w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		itgiccshift.a	. . . . 5 |- ( ph -> A e. RR )
2		itgiccshift.b	. . . . 5 |- ( ph -> B e. RR )
3		itgiccshift.t	. . . . . 6 |- ( ph -> T e. RR+ )
4	3	rpred 11268	. . . . 5 |- ( ph -> T e. RR )
5		itgiccshift.aleb	. . . . 5 |- ( ph -> A <_ B )
6	1, 2, 4, 5	leadd1dd 10178	. . . 4 |- ( ph -> ( A + T ) <_ ( B + T ) )
7	6	ditgpos 22128	. . 3 |- ( ph -> S__ [ ( A + T ) -> ( B + T ) ] ( G ` x ) _d x = S. ( ( A + T ) (,) ( B + T ) ) ( G ` x ) _d x )
8	1, 4	readdcld 9635	. . . 4 |- ( ph -> ( A + T ) e. RR )
9	2, 4	readdcld 9635	. . . 4 |- ( ph -> ( B + T ) e. RR )
10		itgiccshift.f	. . . . . . . . . 10 |- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
11		cncff 21265	. . . . . . . . . 10 |- ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
12	10, 11	syl 16	. . . . . . . . 9 |- ( ph -> F : ( A [,] B ) --> CC )
13	12	adantr 465	. . . . . . . 8 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> F : ( A [,] B ) --> CC )
14	8	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) e. RR )
15	9	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( B + T ) e. RR )
16		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
17		eliccre 31427	. . . . . . . . . . . 12 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
18	14, 15, 16, 17	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. RR )
19	4	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. RR )
20	18, 19	resubcld 9999	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) e. RR )
21		ax-resscn 9561	. . . . . . . . . . . . . . 15 |- RR C_ CC
22	21, 1	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ph -> A e. CC )
23	21, 4	sseldi 3507	. . . . . . . . . . . . . 14 |- ( ph -> T e. CC )
24	22, 23	pncand 9943	. . . . . . . . . . . . 13 |- ( ph -> ( ( A + T ) - T ) = A )
25	24	eqcomd 2475	. . . . . . . . . . . 12 |- ( ph -> A = ( ( A + T ) - T ) )
26	25	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A = ( ( A + T ) - T ) )
27		elicc2 11601	. . . . . . . . . . . . . . 15 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
28	14, 15, 27	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. ( ( A + T ) [,] ( B + T ) ) <-> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) ) )
29	16, 28	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. RR /\ ( A + T ) <_ x /\ x <_ ( B + T ) ) )
30	29	simp2d 1009	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( A + T ) <_ x )
31	14, 18, 19	lesub1d 10171	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) <_ x <-> ( ( A + T ) - T ) <_ ( x - T ) ) )
32	30, 31	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( A + T ) - T ) <_ ( x - T ) )
33	26, 32	eqbrtrd 4473	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A <_ ( x - T ) )
34	29	simp3d 1010	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x <_ ( B + T ) )
35	18, 15, 19	lesub1d 10171	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x <_ ( B + T ) <-> ( x - T ) <_ ( ( B + T ) - T ) ) )
36	34, 35	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ ( ( B + T ) - T ) )
37	21, 2	sseldi 3507	. . . . . . . . . . . . 13 |- ( ph -> B e. CC )
38	37, 23	pncand 9943	. . . . . . . . . . . 12 |- ( ph -> ( ( B + T ) - T ) = B )
39	38	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( B + T ) - T ) = B )
40	36, 39	breqtrd 4477	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) <_ B )
41	20, 33, 40	3jca 1176	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) )
42	1	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> A e. RR )
43	2	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> B e. RR )
44		elicc2 11601	. . . . . . . . . 10 |- ( ( A e. RR /\ B e. RR ) -> ( ( x - T ) e. ( A [,] B ) <-> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) ) )
45	42, 43, 44	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) e. ( A [,] B ) <-> ( ( x - T ) e. RR /\ A <_ ( x - T ) /\ ( x - T ) <_ B ) ) )
46	41, 45	mpbird 232	. . . . . . . 8 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x - T ) e. ( A [,] B ) )
47	13, 46	ffvelrnd 6033	. . . . . . 7 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( F ` ( x - T ) ) e. CC )
48		itgiccshift.g	. . . . . . 7 |- G = ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( x - T ) ) )
49	47, 48	fmptd 6056	. . . . . 6 |- ( ph -> G : ( ( A + T ) [,] ( B + T ) ) --> CC )
50	49	adantr 465	. . . . 5 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> G : ( ( A + T ) [,] ( B + T ) ) --> CC )
51		ffvelrn 6030	. . . . 5 |- ( ( G : ( ( A + T ) [,] ( B + T ) ) --> CC /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( G ` x ) e. CC )
52	50, 16, 51	syl2anc 661	. . . 4 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( G ` x ) e. CC )
53	8, 9, 52	itgioo 22090	. . 3 |- ( ph -> S. ( ( A + T ) (,) ( B + T ) ) ( G ` x ) _d x = S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x )
54	7, 53	eqtr2d 2509	. 2 |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x = S__ [ ( A + T ) -> ( B + T ) ] ( G ` x ) _d x )
55		eqid 2467	. . . 4 |- ( y e. CC |-> ( y + T ) ) = ( y e. CC |-> ( y + T ) )
56	55	addccncf 21288	. . . . 5 |- ( T e. CC -> ( y e. CC |-> ( y + T ) ) e. ( CC -cn-> CC ) )
57	23, 56	syl 16	. . . 4 |- ( ph -> ( y e. CC |-> ( y + T ) ) e. ( CC -cn-> CC ) )
58		iccssre 11618	. . . . . 6 |- ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
59	1, 2, 58	syl2anc 661	. . . . 5 |- ( ph -> ( A [,] B ) C_ RR )
60	59, 21	syl6ss 3521	. . . 4 |- ( ph -> ( A [,] B ) C_ CC )
61		iccssre 11618	. . . . . 6 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( ( A + T ) [,] ( B + T ) ) C_ RR )
62	8, 9, 61	syl2anc 661	. . . . 5 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) C_ RR )
63	21	a1i 11	. . . . 5 |- ( ph -> RR C_ CC )
64	62, 63	sstrd 3519	. . . 4 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) C_ CC )
65	59	sselda 3509	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. RR )
66	4	adantr 465	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> T e. RR )
67	65, 66	readdcld 9635	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) e. RR )
68	1	adantr 465	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> A e. RR )
69		simpr 461	. . . . . . . . 9 |- ( ( ph /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
70	2	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ y e. ( A [,] B ) ) -> B e. RR )
71		elicc2 11601	. . . . . . . . . 10 |- ( ( A e. RR /\ B e. RR ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
72	68, 70, 71	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. ( A [,] B ) <-> ( y e. RR /\ A <_ y /\ y <_ B ) ) )
73	69, 72	mpbid 210	. . . . . . . 8 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y e. RR /\ A <_ y /\ y <_ B ) )
74	73	simp2d 1009	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> A <_ y )
75	68, 65, 66, 74	leadd1dd 10178	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( A + T ) <_ ( y + T ) )
76	73	simp3d 1010	. . . . . . 7 |- ( ( ph /\ y e. ( A [,] B ) ) -> y <_ B )
77	65, 70, 66, 76	leadd1dd 10178	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) <_ ( B + T ) )
78	67, 75, 77	3jca 1176	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( ( y + T ) e. RR /\ ( A + T ) <_ ( y + T ) /\ ( y + T ) <_ ( B + T ) ) )
79	8	adantr 465	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( A + T ) e. RR )
80	9	adantr 465	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( B + T ) e. RR )
81		elicc2 11601	. . . . . 6 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( ( y + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( y + T ) e. RR /\ ( A + T ) <_ ( y + T ) /\ ( y + T ) <_ ( B + T ) ) ) )
82	79, 80, 81	syl2anc 661	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( ( y + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( y + T ) e. RR /\ ( A + T ) <_ ( y + T ) /\ ( y + T ) <_ ( B + T ) ) ) )
83	78, 82	mpbird 232	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( y + T ) e. ( ( A + T ) [,] ( B + T ) ) )
84	55, 57, 60, 64, 83	cncfmptssg 31531	. . 3 |- ( ph -> ( y e. ( A [,] B ) |-> ( y + T ) ) e. ( ( A [,] B ) -cn-> ( ( A + T ) [,] ( B + T ) ) ) )
85		nfcv 2629	. . . . . . . . 9 |- F/_ w ( F ` ( x - T ) )
86		nfcv 2629	. . . . . . . . 9 |- F/_ x ( F ` ( w - T ) )
87		oveq1 6302	. . . . . . . . . 10 |- ( x = w -> ( x - T ) = ( w - T ) )
88	87	fveq2d 5876	. . . . . . . . 9 |- ( x = w -> ( F ` ( x - T ) ) = ( F ` ( w - T ) ) )
89	85, 86, 88	cbvmpt 4543	. . . . . . . 8 |- ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( x - T ) ) ) = ( w e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( w - T ) ) )
90	89	a1i 11	. . . . . . 7 |- ( ph -> ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( x - T ) ) ) = ( w e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( w - T ) ) ) )
91		eqeq1 2471	. . . . . . . . . . . . 13 |- ( w = x -> ( w = ( z + T ) <-> x = ( z + T ) ) )
92	91	rexbidv 2978	. . . . . . . . . . . 12 |- ( w = x -> ( E. z e. ( A [,] B ) w = ( z + T ) <-> E. z e. ( A [,] B ) x = ( z + T ) ) )
93		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( z = y -> ( z + T ) = ( y + T ) )
94	93	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( z = y -> ( x = ( z + T ) <-> x = ( y + T ) ) )
95	94	cbvrexv 3094	. . . . . . . . . . . . 13 |- ( E. z e. ( A [,] B ) x = ( z + T ) <-> E. y e. ( A [,] B ) x = ( y + T ) )
96	95	a1i 11	. . . . . . . . . . . 12 |- ( w = x -> ( E. z e. ( A [,] B ) x = ( z + T ) <-> E. y e. ( A [,] B ) x = ( y + T ) ) )
97	92, 96	bitrd 253	. . . . . . . . . . 11 |- ( w = x -> ( E. z e. ( A [,] B ) w = ( z + T ) <-> E. y e. ( A [,] B ) x = ( y + T ) ) )
98	97	cbvrabv 3117	. . . . . . . . . 10 |- { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) }
99	98	eqcomi 2480	. . . . . . . . 9 |- { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } = { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) }
100		nfv 1683	. . . . . . . . . . 11 |- F/ x ph
101		simpr 461	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
102	92	elrab 3266	. . . . . . . . . . . . . . 15 |- ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
103	101, 102	sylib 196	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
104		simprr 756	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
105		nfv 1683	. . . . . . . . . . . . . . . . . . 19 |- F/ z ph
106		nfv 1683	. . . . . . . . . . . . . . . . . . . 20 |- F/ z x e. CC
107		nfre1 2928	. . . . . . . . . . . . . . . . . . . 20 |- F/ z E. z e. ( A [,] B ) x = ( z + T )
108	106, 107	nfan 1875	. . . . . . . . . . . . . . . . . . 19 |- F/ z ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) )
109	105, 108	nfan 1875	. . . . . . . . . . . . . . . . . 18 |- F/ z ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
110		nfv 1683	. . . . . . . . . . . . . . . . . 18 |- F/ z x e. ( ( A + T ) [,] ( B + T ) )
111		simp3 998	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> x = ( z + T ) )
112	59	sselda 3509	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> z e. RR )
113	4	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> T e. RR )
114	112, 113	readdcld 9635	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) e. RR )
115		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ z e. ( A [,] B ) ) -> z e. ( A [,] B ) )
116	1	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. ( A [,] B ) ) -> A e. RR )
117	2	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ z e. ( A [,] B ) ) -> B e. RR )
118		elicc2 11601	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A e. RR /\ B e. RR ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
119	116, 117, 118	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. ( A [,] B ) <-> ( z e. RR /\ A <_ z /\ z <_ B ) ) )
120	115, 119	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( z e. RR /\ A <_ z /\ z <_ B ) )
121	120	simp2d 1009	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> A <_ z )
122	116, 112, 113	leadd1d 10158	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( A <_ z <-> ( A + T ) <_ ( z + T ) ) )
123	121, 122	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( A + T ) <_ ( z + T ) )
124	120	simp3d 1010	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> z <_ B )
125	112, 117, 113	leadd1d 10158	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( z <_ B <-> ( z + T ) <_ ( B + T ) ) )
126	124, 125	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( z + T ) <_ ( B + T ) )
127	114, 123, 126	3jca 1176	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( A [,] B ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
128	127	3adant3 1016	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( ( z + T ) e. RR /\ ( A + T ) <_ ( z + T ) /\ ( z + T ) <_ ( B + T ) ) )
129	8	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( A + T ) e. RR )
130	9	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( B + T ) e. RR )
131		elicc2 11601	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 ) ) ) )
132	129, 130, 131	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) ) )
133	128, 132	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> ( z + T ) e. ( ( A + T ) [,] ( B + T ) ) )
134	111, 133	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ( A [,] B ) /\ x = ( z + T ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
135	134	3exp 1195	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( z e. ( A [,] B ) -> ( x = ( z + T ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) ) )
136	135	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) )
137	109, 110, 136	rexlimd 2951	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
138	104, 137	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
139	138	ex 434	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) )
140	139	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> ( ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) -> x e. ( ( A + T ) [,] ( B + T ) ) ) )
141	103, 140	mpd 15	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) -> x e. ( ( A + T ) [,] ( B + T ) ) )
142	141	ex 434	. . . . . . . . . . . 12 |- ( ph -> ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } -> x e. ( ( A + T ) [,] ( B + T ) ) ) )
143	21, 18	sseldi 3507	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. CC )
144	23	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> T e. CC )
145	143, 144	npcand 9946	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( ( x - T ) + T ) = x )
146	145	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x = ( ( x - T ) + T ) )
147		oveq1 6302	. . . . . . . . . . . . . . . . . 18 |- ( z = ( x - T ) -> ( z + T ) = ( ( x - T ) + T ) )
148	147	eqeq2d 2481	. . . . . . . . . . . . . . . . 17 |- ( z = ( x - T ) -> ( x = ( z + T ) <-> x = ( ( x - T ) + T ) ) )
149	148	rspcev 3219	. . . . . . . . . . . . . . . 16 |- ( ( ( x - T ) e. ( A [,] B ) /\ x = ( ( x - T ) + T ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
150	46, 146, 149	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> E. z e. ( A [,] B ) x = ( z + T ) )
151	143, 150	jca 532	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> ( x e. CC /\ E. z e. ( A [,] B ) x = ( z + T ) ) )
152	151, 102	sylibr 212	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. ( ( A + T ) [,] ( B + T ) ) ) -> x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } )
153	152	ex 434	. . . . . . . . . . . 12 |- ( ph -> ( x e. ( ( A + T ) [,] ( B + T ) ) -> x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } ) )
154	142, 153	impbid 191	. . . . . . . . . . 11 |- ( ph -> ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> x e. ( ( A + T ) [,] ( B + T ) ) ) )
155	100, 154	alrimi 1825	. . . . . . . . . 10 |- ( ph -> A. x ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> x e. ( ( A + T ) [,] ( B + T ) ) ) )
156		dfcleq 2460	. . . . . . . . . 10 |- ( { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = ( ( A + T ) [,] ( B + T ) ) <-> A. x ( x e. { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } <-> x e. ( ( A + T ) [,] ( B + T ) ) ) )
157	155, 156	sylibr 212	. . . . . . . . 9 |- ( ph -> { w e. CC | E. z e. ( A [,] B ) w = ( z + T ) } = ( ( A + T ) [,] ( B + T ) ) )
158	99, 157	syl5req 2521	. . . . . . . 8 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } )
159	158	mpteq1d 4534	. . . . . . 7 |- ( 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 ) ) ) )
160	90, 159	eqtrd 2508	. . . . . 6 |- ( 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 ) ) ) )
161	48, 160	syl5eq 2520	. . . . 5 |- ( ph -> G = ( w e. { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } |-> ( F ` ( w - T ) ) ) )
162		eqid 2467	. . . . . 6 |- ( 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 ) ) )
163	60, 23, 99, 10, 162	cncfshift 31535	. . . . 5 |- ( 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 ) )
164	161, 163	eqeltrd 2555	. . . 4 |- ( ph -> G e. ( { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } -cn-> CC ) )
165	49	feqmptd 5927	. . . . 5 |- ( ph -> G = ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( G ` x ) ) )
166	1, 2, 4	iccshift 31445	. . . . . . 7 |- ( ph -> ( ( A + T ) [,] ( B + T ) ) = { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } )
167	166	eqcomd 2475	. . . . . 6 |- ( ph -> { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } = ( ( A + T ) [,] ( B + T ) ) )
168		eqidd 2468	. . . . . 6 |- ( ph -> CC = CC )
169	167, 168	oveq12d 6313	. . . . 5 |- ( ph -> ( { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } -cn-> CC ) = ( ( ( A + T ) [,] ( B + T ) ) -cn-> CC ) )
170	165, 169	eleq12d 2549	. . . 4 |- ( ph -> ( G e. ( { x e. CC | E. y e. ( A [,] B ) x = ( y + T ) } -cn-> CC ) <-> ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( G ` x ) ) e. ( ( ( A + T ) [,] ( B + T ) ) -cn-> CC ) ) )
171	164, 170	mpbid 210	. . 3 |- ( ph -> ( x e. ( ( A + T ) [,] ( B + T ) ) |-> ( G ` x ) ) e. ( ( ( A + T ) [,] ( B + T ) ) -cn-> CC ) )
172		ax-1cn 9562	. . . . . . 7 |- 1 e. CC
173	172	a1i 11	. . . . . 6 |- ( ph -> 1 e. CC )
174		ioosscn 31414	. . . . . . 7 |- ( A (,) B ) C_ CC
175	174	a1i 11	. . . . . 6 |- ( ph -> ( A (,) B ) C_ CC )
176		ssid 3528	. . . . . . 7 |- CC C_ CC
177	176	a1i 11	. . . . . 6 |- ( ph -> CC C_ CC )
178		cncfmptc 21283	. . . . . 6 |- ( ( 1 e. CC /\ ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( y e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
179	173, 175, 177, 178	syl3anc 1228	. . . . 5 |- ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
180		fconstmpt 5049	. . . . . . . 8 |- ( ( A (,) B ) X. { 1 } ) = ( y e. ( A (,) B ) |-> 1 )
181	180	eqcomi 2480	. . . . . . 7 |- ( y e. ( A (,) B ) |-> 1 ) = ( ( A (,) B ) X. { 1 } )
182	181	a1i 11	. . . . . 6 |- ( ph -> ( y e. ( A (,) B ) |-> 1 ) = ( ( A (,) B ) X. { 1 } ) )
183		ioombl 21843	. . . . . . . 8 |- ( A (,) B ) e. dom vol
184	183	a1i 11	. . . . . . 7 |- ( ph -> ( A (,) B ) e. dom vol )
185		ioovolcl 21847	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR ) -> ( vol ` ( A (,) B ) ) e. RR )
186	1, 2, 185	syl2anc 661	. . . . . . 7 |- ( ph -> ( vol ` ( A (,) B ) ) e. RR )
187		iblconst 22092	. . . . . . 7 |- ( ( ( A (,) B ) e. dom vol /\ ( vol ` ( A (,) B ) ) e. RR /\ 1 e. CC ) -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
188	184, 186, 173, 187	syl3anc 1228	. . . . . 6 |- ( ph -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
189	182, 188	eqeltrd 2555	. . . . 5 |- ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. L^1 )
190	179, 189	jca 532	. . . 4 |- ( ph -> ( ( y e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) /\ ( y e. ( A (,) B ) |-> 1 ) e. L^1 ) )
191		elin 3692	. . . 4 |- ( ( y e. ( A (,) B ) |-> 1 ) e. ( ( ( A (,) B ) -cn-> CC ) i^i L^1 ) <-> ( ( y e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) /\ ( y e. ( A (,) B ) |-> 1 ) e. L^1 ) )
192	190, 191	sylibr 212	. . 3 |- ( ph -> ( y e. ( A (,) B ) |-> 1 ) e. ( ( ( A (,) B ) -cn-> CC ) i^i L^1 ) )
193		resmpt 5329	. . . . . . . 8 |- ( ( A [,] B ) C_ RR -> ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) = ( y e. ( A [,] B ) |-> ( y + T ) ) )
194	59, 193	syl 16	. . . . . . 7 |- ( ph -> ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) = ( y e. ( A [,] B ) |-> ( y + T ) ) )
195	194	eqcomd 2475	. . . . . 6 |- ( ph -> ( y e. ( A [,] B ) |-> ( y + T ) ) = ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) )
196	195	oveq2d 6311	. . . . 5 |- ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( RR _D ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) ) )
197	63	sselda 3509	. . . . . . . . 9 |- ( ( ph /\ y e. RR ) -> y e. CC )
198	23	adantr 465	. . . . . . . . 9 |- ( ( ph /\ y e. RR ) -> T e. CC )
199	197, 198	addcld 9627	. . . . . . . 8 |- ( ( ph /\ y e. RR ) -> ( y + T ) e. CC )
200		eqid 2467	. . . . . . . 8 |- ( y e. RR |-> ( y + T ) ) = ( y e. RR |-> ( y + T ) )
201	199, 200	fmptd 6056	. . . . . . 7 |- ( ph -> ( y e. RR |-> ( y + T ) ) : RR --> CC )
202	63, 201	jca 532	. . . . . 6 |- ( ph -> ( RR C_ CC /\ ( y e. RR |-> ( y + T ) ) : RR --> CC ) )
203		ssid 3528	. . . . . . . 8 |- RR C_ RR
204	203	a1i 11	. . . . . . 7 |- ( ph -> RR C_ RR )
205	204, 59	jca 532	. . . . . 6 |- ( ph -> ( RR C_ RR /\ ( A [,] B ) C_ RR ) )
206		eqid 2467	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
207	206	tgioo2 21176	. . . . . . 7 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
208	206, 207	dvres 22183	. . . . . 6 |- ( ( ( 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 ) ) ) )
209	202, 205, 208	syl2anc 661	. . . . 5 |- ( ph -> ( RR _D ( ( y e. RR |-> ( y + T ) ) |` ( A [,] B ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
210	196, 209	eqtrd 2508	. . . 4 |- ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) )
211		iccntr 21194	. . . . . 6 |- ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
212	1, 2, 211	syl2anc 661	. . . . 5 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
213	212	reseq2d 5279	. . . 4 |- ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) ) = ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) )
214		reex 9595	. . . . . . . . 9 |- RR e. _V
215	214	prid1 4141	. . . . . . . 8 |- RR e. { RR , CC }
216	215	a1i 11	. . . . . . 7 |- ( ph -> RR e. { RR , CC } )
217	172	a1i 11	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> 1 e. CC )
218	216	dvmptid 22228	. . . . . . 7 |- ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
219		0cn 9600	. . . . . . . 8 |- 0 e. CC
220	219	a1i 11	. . . . . . 7 |- ( ( ph /\ y e. RR ) -> 0 e. CC )
221	216, 23	dvmptc 22229	. . . . . . 7 |- ( ph -> ( RR _D ( y e. RR |-> T ) ) = ( y e. RR |-> 0 ) )
222	216, 197, 217, 218, 198, 220, 221	dvmptadd 22231	. . . . . 6 |- ( ph -> ( RR _D ( y e. RR |-> ( y + T ) ) ) = ( y e. RR |-> ( 1 + 0 ) ) )
223	222	reseq1d 5278	. . . . 5 |- ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) = ( ( y e. RR |-> ( 1 + 0 ) ) |` ( A (,) B ) ) )
224		ioossre 11598	. . . . . . 7 |- ( A (,) B ) C_ RR
225	224	a1i 11	. . . . . 6 |- ( ph -> ( A (,) B ) C_ RR )
226		resmpt 5329	. . . . . 6 |- ( ( A (,) B ) C_ RR -> ( ( y e. RR |-> ( 1 + 0 ) ) |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) )
227	225, 226	syl 16	. . . . 5 |- ( ph -> ( ( y e. RR |-> ( 1 + 0 ) ) |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) )
228	172	addid1i 9778	. . . . . . 7 |- ( 1 + 0 ) = 1
229	228	mpteq2i 4536	. . . . . 6 |- ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) = ( y e. ( A (,) B ) |-> 1 )
230	229	a1i 11	. . . . 5 |- ( ph -> ( y e. ( A (,) B ) |-> ( 1 + 0 ) ) = ( y e. ( A (,) B ) |-> 1 ) )
231	223, 227, 230	3eqtrd 2512	. . . 4 |- ( ph -> ( ( RR _D ( y e. RR |-> ( y + T ) ) ) |` ( A (,) B ) ) = ( y e. ( A (,) B ) |-> 1 ) )
232	210, 213, 231	3eqtrd 2512	. . 3 |- ( ph -> ( RR _D ( y e. ( A [,] B ) |-> ( y + T ) ) ) = ( y e. ( A (,) B ) |-> 1 ) )
233		fveq2 5872	. . 3 |- ( x = ( y + T ) -> ( G ` x ) = ( G ` ( y + T ) ) )
234		oveq1 6302	. . 3 |- ( y = A -> ( y + T ) = ( A + T ) )
235		oveq1 6302	. . 3 |- ( y = B -> ( y + T ) = ( B + T ) )
236	1, 2, 5, 84, 171, 192, 232, 233, 234, 235, 8, 9	itgsubsticc 31617	. 2 |- ( ph -> S__ [ ( A + T ) -> ( B + T ) ] ( G ` x ) _d x = S__ [ A -> B ] ( ( G ` ( y + T ) ) x. 1 ) _d y )
237	5	ditgpos 22128	. . 3 |- ( ph -> S__ [ A -> B ] ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A (,) B ) ( ( G ` ( y + T ) ) x. 1 ) _d y )
238	49	adantr 465	. . . . . 6 |- ( ( ph /\ y e. ( A [,] B ) ) -> G : ( ( A + T ) [,] ( B + T ) ) --> CC )
239		ffvelrn 6030	. . . . . 6 |- ( ( G : ( ( A + T ) [,] ( B + T ) ) --> CC /\ ( y + T ) e. ( ( A + T ) [,] ( B + T ) ) ) -> ( G ` ( y + T ) ) e. CC )
240	238, 83, 239	syl2anc 661	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( G ` ( y + T ) ) e. CC )
241	172	a1i 11	. . . . 5 |- ( ( ph /\ y e. ( A [,] B ) ) -> 1 e. CC )
242	240, 241	mulcld 9628	. . . 4 |- ( ( ph /\ y e. ( A [,] B ) ) -> ( ( G ` ( y + T ) ) x. 1 ) e. CC )
243	1, 2, 242	itgioo 22090	. . 3 |- ( ph -> S. ( A (,) B ) ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( ( G ` ( y + T ) ) x. 1 ) _d y )
244		oveq1 6302	. . . . . . . 8 |- ( y = x -> ( y + T ) = ( x + T ) )
245	244	fveq2d 5876	. . . . . . 7 |- ( y = x -> ( G ` ( y + T ) ) = ( G ` ( x + T ) ) )
246	245	oveq1d 6310	. . . . . 6 |- ( y = x -> ( ( G ` ( y + T ) ) x. 1 ) = ( ( G ` ( x + T ) ) x. 1 ) )
247		nfcv 2629	. . . . . 6 |- F/_ x ( ( G ` ( y + T ) ) x. 1 )
248		nfcv 2629	. . . . . 6 |- F/_ y ( ( G ` ( x + T ) ) x. 1 )
249	246, 247, 248	cbvitg 22050	. . . . 5 |- S. ( A [,] B ) ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( ( G ` ( x + T ) ) x. 1 ) _d x
250	249	a1i 11	. . . 4 |- ( ph -> S. ( A [,] B ) ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( ( G ` ( x + T ) ) x. 1 ) _d x )
251	49	adantr 465	. . . . . . . 8 |- ( ( ph /\ x e. ( A [,] B ) ) -> G : ( ( A + T ) [,] ( B + T ) ) --> CC )
252	59	sselda 3509	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
253	4	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> T e. RR )
254	252, 253	readdcld 9635	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x + T ) e. RR )
255	1	rexrd 9655	. . . . . . . . . . . . 13 |- ( ph -> A e. RR* )
256	255	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR* )
257	2	rexrd 9655	. . . . . . . . . . . . 13 |- ( ph -> B e. RR* )
258	257	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR* )
259		simpr 461	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
260		iccgelb 11593	. . . . . . . . . . . 12 |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> A <_ x )
261	256, 258, 259, 260	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
262	1	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
263	262, 252, 253	leadd1d 10158	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( A <_ x <-> ( A + T ) <_ ( x + T ) ) )
264	261, 263	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( A + T ) <_ ( x + T ) )
265		iccleub 11592	. . . . . . . . . . . 12 |- ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> x <_ B )
266	256, 258, 259, 265	syl3anc 1228	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
267	2	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
268	252, 267, 253	leadd1d 10158	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x <_ B <-> ( x + T ) <_ ( B + T ) ) )
269	266, 268	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x + T ) <_ ( B + T ) )
270	254, 264, 269	3jca 1176	. . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( ( x + T ) e. RR /\ ( A + T ) <_ ( x + T ) /\ ( x + T ) <_ ( B + T ) ) )
271	8	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( A + T ) e. RR )
272	9	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( B + T ) e. RR )
273		elicc2 11601	. . . . . . . . . 10 |- ( ( ( A + T ) e. RR /\ ( B + T ) e. RR ) -> ( ( x + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( x + T ) e. RR /\ ( A + T ) <_ ( x + T ) /\ ( x + T ) <_ ( B + T ) ) ) )
274	271, 272, 273	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( ( x + T ) e. ( ( A + T ) [,] ( B + T ) ) <-> ( ( x + T ) e. RR /\ ( A + T ) <_ ( x + T ) /\ ( x + T ) <_ ( B + T ) ) ) )
275	270, 274	mpbird 232	. . . . . . . 8 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( x + T ) e. ( ( A + T ) [,] ( B + T ) ) )
276	251, 275	ffvelrnd 6033	. . . . . . 7 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( G ` ( x + T ) ) e. CC )
277	276	mulid1d 9625	. . . . . 6 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( ( G ` ( x + T ) ) x. 1 ) = ( G ` ( x + T ) ) )
278	48, 89	eqtri 2496	. . . . . . . 8 |- G = ( w e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( w - T ) ) )
279	278	a1i 11	. . . . . . 7 |- ( ( ph /\ x e. ( A [,] B ) ) -> G = ( w e. ( ( A + T ) [,] ( B + T ) ) |-> ( F ` ( w - T ) ) ) )
280		oveq1 6302	. . . . . . . . . 10 |- ( w = ( x + T ) -> ( w - T ) = ( ( x + T ) - T ) )
281	280	fveq2d 5876	. . . . . . . . 9 |- ( w = ( x + T ) -> ( F ` ( w - T ) ) = ( F ` ( ( x + T ) - T ) ) )
282	281	adantl 466	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ w = ( x + T ) ) -> ( F ` ( w - T ) ) = ( F ` ( ( x + T ) - T ) ) )
283	21, 252	sseldi 3507	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> x e. CC )
284	23	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A [,] B ) ) -> T e. CC )
285	283, 284	pncand 9943	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( ( x + T ) - T ) = x )
286	285	fveq2d 5876	. . . . . . . . 9 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` ( ( x + T ) - T ) ) = ( F ` x ) )
287	286	adantr 465	. . . . . . . 8 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ w = ( x + T ) ) -> ( F ` ( ( x + T ) - T ) ) = ( F ` x ) )
288	282, 287	eqtrd 2508	. . . . . . 7 |- ( ( ( ph /\ x e. ( A [,] B ) ) /\ w = ( x + T ) ) -> ( F ` ( w - T ) ) = ( F ` x ) )
289	12	ffvelrnda 6032	. . . . . . 7 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) e. CC )
290	279, 288, 275, 289	fvmptd 5962	. . . . . 6 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( G ` ( x + T ) ) = ( F ` x ) )
291	277, 290	eqtrd 2508	. . . . 5 |- ( ( ph /\ x e. ( A [,] B ) ) -> ( ( G ` ( x + T ) ) x. 1 ) = ( F ` x ) )
292	291	itgeq2dv 22056	. . . 4 |- ( ph -> S. ( A [,] B ) ( ( G ` ( x + T ) ) x. 1 ) _d x = S. ( A [,] B ) ( F ` x ) _d x )
293	250, 292	eqtrd 2508	. . 3 |- ( ph -> S. ( A [,] B ) ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( F ` x ) _d x )
294	237, 243, 293	3eqtrd 2512	. 2 |- ( ph -> S__ [ A -> B ] ( ( G ` ( y + T ) ) x. 1 ) _d y = S. ( A [,] B ) ( F ` x ) _d x )
295	54, 236, 294	3eqtrd 2512	1 |- ( ph -> S. ( ( A + T ) [,] ( B + T ) ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   A.wal 1377   = wceq 1379   e. wcel 1767   E.wrex 2818   {crab 2821   i^i cin 3480   C_ wss 3481   {csn 4033   {cpr 4035   class class class wbr 4453   |-> cmpt 4511   X. cxp 5003   dom cdm 5005   ran crn 5006   |` cres 5007   -->wf 5590   ` cfv 5594  (class class class)co 6295   CCcc 9502   RRcr 9503   0cc0 9504   1c1 9505   + caddc 9507   x. cmul 9509   RR*cxr 9639   <_ cle 9641   - cmin 9817   RR+crp 11232   (,)cioo 11541   [,]cicc 11544   TopOpenctopn 14694   topGenctg 14710  ℂ_fldccnfld 18290   intcnt 19386   -cn->ccncf 21248   volcvol 21743   L^1cibl 21894   S.citg 21895   S__cdit 22118   _D cdv 22135

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-inf2 8070  ax-cc 8827  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582  ax-addf 9583  ax-mulf 9584

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-int 4289  df-iun 4333  df-iin 4334  df-disj 4424  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-se 4845  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-isom 5603  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-of 6535  df-ofr 6536  df-om 6696  df-1st 6795  df-2nd 6796  df-supp 6914  df-recs 7054  df-rdg 7088  df-1o 7142  df-2o 7143  df-oadd 7146  df-omul 7147  df-er 7323  df-map 7434  df-pm 7435  df-ixp 7482  df-en 7529  df-dom 7530  df-sdom 7531  df-fin 7532  df-fsupp 7842  df-fi 7883  df-sup 7913  df-oi 7947  df-card 8332  df-acn 8335  df-cda 8560  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-4 10608  df-5 10609  df-6 10610  df-7 10611  df-8 10612  df-9 10613  df-10 10614  df-n0 10808  df-z 10877  df-dec 10989  df-uz 11095  df-q 11195  df-rp 11233  df-xneg 11330  df-xadd 11331  df-xmul 11332  df-ioo 11545  df-ioc 11546  df-ico 11547  df-icc 11548  df-fz 11685  df-fzo 11805  df-fl 11909  df-mod 11977  df-seq 12088  df-exp 12147  df-hash 12386  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-limsup 13274  df-clim 13291  df-rlim 13292  df-sum 13489  df-struct 14509  df-ndx 14510  df-slot 14511  df-base 14512  df-sets 14513  df-ress 14514  df-plusg 14585  df-mulr 14586  df-starv 14587  df-sca 14588  df-vsca 14589  df-ip 14590  df-tset 14591  df-ple 14592  df-ds 14594  df-unif 14595  df-hom 14596  df-cco 14597  df-rest 14695  df-topn 14696  df-0g 14714  df-gsum 14715  df-topgen 14716  df-pt 14717  df-prds 14720  df-xrs 14774  df-qtop 14779  df-imas 14780  df-xps 14782  df-mre 14858  df-mrc 14859  df-acs 14861  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-submnd 15840  df-mulg 15932  df-cntz 16227  df-cmn 16673  df-psmet 18281  df-xmet 18282  df-met 18283  df-bl 18284  df-mopn 18285  df-fbas 18286  df-fg 18287  df-cnfld 18291  df-top 19268  df-bases 19270  df-topon 19271  df-topsp 19272  df-cld 19388  df-ntr 19389  df-cls 19390  df-nei 19467  df-lp 19505  df-perf 19506  df-cn 19596  df-cnp 19597  df-haus 19684  df-cmp 19755  df-tx 19931  df-hmeo 20124  df-fil 20215  df-fm 20307  df-flim 20308  df-flf 20309  df-xms 20691  df-ms 20692  df-tms 20693  df-cncf 21250  df-ovol 21744  df-vol 21745  df-mbf 21896  df-itg1 21897  df-itg2 21898  df-ibl 21899  df-itg 21900  df-0p 21945  df-ditg 22119  df-limc 22138  df-dv 22139

This theorem is referenced by:  fourierdlem81  31811