fourierdlem108

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by any positive value X . This lemma generalizes fourierdlem92 where the integral was shifted by the exact period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem108.a	\|- ( ph -> A e. RR )
	fourierdlem108.b	\|- ( ph -> B e. RR )
	fourierdlem108.t	\|- T = ( B - A )
	fourierdlem108.x	\|- ( ph -> X e. RR+ )
	fourierdlem108.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem108.m	\|- ( ph -> M e. NN )
	fourierdlem108.q	\|- ( ph -> Q e. ( P ` M ) )
	fourierdlem108.f	\|- ( ph -> F : RR --> CC )
	fourierdlem108.fper	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
	fourierdlem108.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem108.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
	fourierdlem108.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
Assertion	fourierdlem108	\|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem108.a	\|- ( ph -> A e. RR )
2		fourierdlem108.b	\|- ( ph -> B e. RR )
3		fourierdlem108.t	\|- T = ( B - A )
4		fourierdlem108.x	\|- ( ph -> X e. RR+ )
5		fourierdlem108.p	\|- P = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = A /\ ( p ` m ) = B ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
6		fourierdlem108.m	\|- ( ph -> M e. NN )
7		fourierdlem108.q	\|- ( ph -> Q e. ( P ` M ) )
8		fourierdlem108.f	\|- ( ph -> F : RR --> CC )
9		fourierdlem108.fper	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10		fourierdlem108.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11		fourierdlem108.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
12		fourierdlem108.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
13		eqid	\|- ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = A ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = ( A - X ) /\ ( p ` m ) = A ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
14		oveq1	\|- ( w = y -> ( w + ( k x. T ) ) = ( y + ( k x. T ) ) )
15	14	eleq1d	\|- ( w = y -> ( ( w + ( k x. T ) ) e. ran Q <-> ( y + ( k x. T ) ) e. ran Q ) )
16	15	rexbidv	\|- ( w = y -> ( E. k e. ZZ ( w + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. T ) ) e. ran Q ) )
17	16	cbvrabv	\|- { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } = { y e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q }
18	17	uneq2i	\|- ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) = ( { ( A - X ) , A } u. { y e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
19		oveq1	\|- ( l = k -> ( l x. T ) = ( k x. T ) )
20	19	oveq2d	\|- ( l = k -> ( w + ( l x. T ) ) = ( w + ( k x. T ) ) )
21	20	eleq1d	\|- ( l = k -> ( ( w + ( l x. T ) ) e. ran Q <-> ( w + ( k x. T ) ) e. ran Q ) )
22	21	cbvrexvw	\|- ( E. l e. ZZ ( w + ( l x. T ) ) e. ran Q <-> E. k e. ZZ ( w + ( k x. T ) ) e. ran Q )
23	22	rgenw	\|- A. w e. ( ( A - X ) [,] A ) ( E. l e. ZZ ( w + ( l x. T ) ) e. ran Q <-> E. k e. ZZ ( w + ( k x. T ) ) e. ran Q )
24		rabbi	\|- ( A. w e. ( ( A - X ) [,] A ) ( E. l e. ZZ ( w + ( l x. T ) ) e. ran Q <-> E. k e. ZZ ( w + ( k x. T ) ) e. ran Q ) <-> { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } = { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
25	23 24	mpbi	\|- { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } = { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q }
26	25	uneq2i	\|- ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) = ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } )
27	26	fveq2i	\|- ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) = ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) )
28	27	oveq1i	\|- ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) - 1 )
29		isoeq5	\|- ( ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) = ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
30	26 29	ax-mp	\|- ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
31		isoeq1	\|- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
32	30 31	bitrid	\|- ( g = f -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) <-> f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) ) )
33	32	cbviotavw	\|- ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) ) = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. l e. ZZ ( w + ( l x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { ( A - X ) , A } u. { w e. ( ( A - X ) [,] A ) \| E. k e. ZZ ( w + ( k x. T ) ) e. ran Q } ) ) )
34		id	\|- ( w = x -> w = x )
35		oveq2	\|- ( w = x -> ( B - w ) = ( B - x ) )
36	35	oveq1d	\|- ( w = x -> ( ( B - w ) / T ) = ( ( B - x ) / T ) )
37	36	fveq2d	\|- ( w = x -> ( \|_ ` ( ( B - w ) / T ) ) = ( \|_ ` ( ( B - x ) / T ) ) )
38	37	oveq1d	\|- ( w = x -> ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) = ( ( \|_ ` ( ( B - x ) / T ) ) x. T ) )
39	34 38	oveq12d	\|- ( w = x -> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) = ( x + ( ( \|_ ` ( ( B - x ) / T ) ) x. T ) ) )
40	39	cbvmptv	\|- ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) = ( x e. RR \|-> ( x + ( ( \|_ ` ( ( B - x ) / T ) ) x. T ) ) )
41		eqeq1	\|- ( w = y -> ( w = B <-> y = B ) )
42		id	\|- ( w = y -> w = y )
43	41 42	ifbieq2d	\|- ( w = y -> if ( w = B , A , w ) = if ( y = B , A , y ) )
44	43	cbvmptv	\|- ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) = ( y e. ( A (,] B ) \|-> if ( y = B , A , y ) )
45		fveq2	\|- ( z = x -> ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) = ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) )
46	45	fveq2d	\|- ( z = x -> ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) = ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) )
47	46	breq2d	\|- ( z = x -> ( ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) <-> ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) ) )
48	47	rabbidv	\|- ( z = x -> { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) } = { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) } )
49		fveq2	\|- ( j = i -> ( Q ` j ) = ( Q ` i ) )
50	49	breq1d	\|- ( j = i -> ( ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) <-> ( Q ` i ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) ) )
51	50	cbvrabv	\|- { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) } = { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) }
52	48 51	eqtrdi	\|- ( z = x -> { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) } = { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) } )
53	52	supeq1d	\|- ( z = x -> sup ( { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
54	53	cbvmptv	\|- ( z e. RR \|-> sup ( { j e. ( 0 ..^ M ) \| ( Q ` j ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` z ) ) } , RR , < ) ) = ( x e. RR \|-> sup ( { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( ( w e. ( A (,] B ) \|-> if ( w = B , A , w ) ) ` ( ( w e. RR \|-> ( w + ( ( \|_ ` ( ( B - w ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
55	1 2 3 4 5 6 7 8 9 10 11 12 13 18 28 33 40 44 54	fourierdlem107	\|- ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x )

Metamath Proof Explorer

Theorem fourierdlem108

Proof