fourierdlem100

Description: A piecewise continuous function is integrable on any closed interval. This lemma uses local definitions, so that the proof is more readable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierlemiblglemlem.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 ) ) ) } )
	fourierdlem100.t	\|- T = ( B - A )
	fourierdlem100.m	\|- ( ph -> M e. NN )
	fourierdlem100.q	\|- ( ph -> Q e. ( P ` M ) )
	fourierdlem100.f	\|- ( ph -> F : RR --> CC )
	fourierdlem100.per	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
	fourierdlem100.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
	fourierdlem100.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
	fourierdlem100.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
	fourierdlem100.c	\|- ( ph -> C e. RR )
	fourierdlem100.d	\|- ( ph -> D e. ( C (,) +oo ) )
	fourierdlem100.o	\|- O = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
	fourierdlem100.n	\|- N = ( ( # ` H ) - 1 )
	fourierdlem100.h	\|- H = ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
	fourierdlem100.s	\|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
	fourierdlem100.e	\|- E = ( x e. RR \|-> ( x + ( ( \|_ ` ( ( B - x ) / T ) ) x. T ) ) )
	fourierdlem100.j	\|- J = ( y e. ( A (,] B ) \|-> if ( y = B , A , y ) )
	fourierdlem100.i	\|- I = ( x e. RR \|-> sup ( { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
Assertion	fourierdlem100	\|- ( ph -> ( x e. ( C [,] D ) \|-> ( F ` x ) ) e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		fourierlemiblglemlem.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 ) ) ) } )
2		fourierdlem100.t	\|- T = ( B - A )
3		fourierdlem100.m	\|- ( ph -> M e. NN )
4		fourierdlem100.q	\|- ( ph -> Q e. ( P ` M ) )
5		fourierdlem100.f	\|- ( ph -> F : RR --> CC )
6		fourierdlem100.per	\|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7		fourierdlem100.fcn	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
8		fourierdlem100.r	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
9		fourierdlem100.l	\|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
10		fourierdlem100.c	\|- ( ph -> C e. RR )
11		fourierdlem100.d	\|- ( ph -> D e. ( C (,) +oo ) )
12		fourierdlem100.o	\|- O = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
13		fourierdlem100.n	\|- N = ( ( # ` H ) - 1 )
14		fourierdlem100.h	\|- H = ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } )
15		fourierdlem100.s	\|- S = ( iota f f Isom < , < ( ( 0 ... N ) , H ) )
16		fourierdlem100.e	\|- E = ( x e. RR \|-> ( x + ( ( \|_ ` ( ( B - x ) / T ) ) x. T ) ) )
17		fourierdlem100.j	\|- J = ( y e. ( A (,] B ) \|-> if ( y = B , A , y ) )
18		fourierdlem100.i	\|- I = ( x e. RR \|-> sup ( { i e. ( 0 ..^ M ) \| ( Q ` i ) <_ ( J ` ( E ` x ) ) } , RR , < ) )
19		elioore	\|- ( D e. ( C (,) +oo ) -> D e. RR )
20	11 19	syl	\|- ( ph -> D e. RR )
21	10 20	iccssred	\|- ( ph -> ( C [,] D ) C_ RR )
22	5 21	feqresmpt	\|- ( ph -> ( F \|` ( C [,] D ) ) = ( x e. ( C [,] D ) \|-> ( F ` x ) ) )
23		fveq2	\|- ( i = j -> ( p ` i ) = ( p ` j ) )
24		oveq1	\|- ( i = j -> ( i + 1 ) = ( j + 1 ) )
25	24	fveq2d	\|- ( i = j -> ( p ` ( i + 1 ) ) = ( p ` ( j + 1 ) ) )
26	23 25	breq12d	\|- ( i = j -> ( ( p ` i ) < ( p ` ( i + 1 ) ) <-> ( p ` j ) < ( p ` ( j + 1 ) ) ) )
27	26	cbvralvw	\|- ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) )
28	27	anbi2i	\|- ( ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) )
29	28	a1i	\|- ( p e. ( RR ^m ( 0 ... m ) ) -> ( ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) ) )
30	29	rabbiia	\|- { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) }
31	30	mpteq2i	\|- ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
32	12 31	eqtri	\|- O = ( m e. NN \|-> { p e. ( RR ^m ( 0 ... m ) ) \| ( ( ( p ` 0 ) = C /\ ( p ` m ) = D ) /\ A. j e. ( 0 ..^ m ) ( p ` j ) < ( p ` ( j + 1 ) ) ) } )
33		elioo4g	\|- ( D e. ( C (,) +oo ) <-> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
34	11 33	sylib	\|- ( ph -> ( ( C e. RR* /\ +oo e. RR* /\ D e. RR ) /\ ( C < D /\ D < +oo ) ) )
35	34	simprd	\|- ( ph -> ( C < D /\ D < +oo ) )
36	35	simpld	\|- ( ph -> C < D )
37		id	\|- ( y = x -> y = x )
38	2	eqcomi	\|- ( B - A ) = T
39	38	oveq2i	\|- ( k x. ( B - A ) ) = ( k x. T )
40	39	a1i	\|- ( y = x -> ( k x. ( B - A ) ) = ( k x. T ) )
41	37 40	oveq12d	\|- ( y = x -> ( y + ( k x. ( B - A ) ) ) = ( x + ( k x. T ) ) )
42	41	eleq1d	\|- ( y = x -> ( ( y + ( k x. ( B - A ) ) ) e. ran Q <-> ( x + ( k x. T ) ) e. ran Q ) )
43	42	rexbidv	\|- ( y = x -> ( E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q <-> E. k e. ZZ ( x + ( k x. T ) ) e. ran Q ) )
44	43	cbvrabv	\|- { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } = { x e. ( C [,] D ) \| E. k e. ZZ ( x + ( k x. T ) ) e. ran Q }
45	44	uneq2i	\|- ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) \| E. k e. ZZ ( x + ( k x. T ) ) e. ran Q } )
46	39	eqcomi	\|- ( k x. T ) = ( k x. ( B - A ) )
47	46	oveq2i	\|- ( y + ( k x. T ) ) = ( y + ( k x. ( B - A ) ) )
48	47	eleq1i	\|- ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( k x. ( B - A ) ) ) e. ran Q )
49	48	rexbii	\|- ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
50	49	rgenw	\|- A. y e. ( C [,] D ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q )
51		rabbi	\|- ( A. y e. ( C [,] D ) ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q ) <-> { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
52	50 51	mpbi	\|- { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q }
53	52	uneq2i	\|- ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
54	14 53	eqtri	\|- H = ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } )
55	54	fveq2i	\|- ( # ` H ) = ( # ` ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) )
56	55	oveq1i	\|- ( ( # ` H ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
57	13 56	eqtri	\|- N = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) - 1 )
58		isoeq5	\|- ( H = ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) -> ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
59	54 58	ax-mp	\|- ( f Isom < , < ( ( 0 ... N ) , H ) <-> f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
60	59	iotabii	\|- ( iota f f Isom < , < ( ( 0 ... N ) , H ) ) = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
61	15 60	eqtri	\|- S = ( iota f f Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) )
62	2 1 3 4 10 20 36 12 45 57 61	fourierdlem54	\|- ( ph -> ( ( N e. NN /\ S e. ( O ` N ) ) /\ S Isom < , < ( ( 0 ... N ) , ( { C , D } u. { y e. ( C [,] D ) \| E. k e. ZZ ( y + ( k x. ( B - A ) ) ) e. ran Q } ) ) ) )
63	62	simpld	\|- ( ph -> ( N e. NN /\ S e. ( O ` N ) ) )
64	63	simpld	\|- ( ph -> N e. NN )
65	63	simprd	\|- ( ph -> S e. ( O ` N ) )
66	5 21	fssresd	\|- ( ph -> ( F \|` ( C [,] D ) ) : ( C [,] D ) --> CC )
67		ioossicc	\|- ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( ( S ` j ) [,] ( S ` ( j + 1 ) ) )
68	10	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> C e. RR )
69	68	rexrd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> C e. RR* )
70	11	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> D e. ( C (,) +oo ) )
71	70 19	syl	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> D e. RR )
72	71	rexrd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> D e. RR* )
73	12 64 65	fourierdlem15	\|- ( ph -> S : ( 0 ... N ) --> ( C [,] D ) )
74	73	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> S : ( 0 ... N ) --> ( C [,] D ) )
75		simpr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> j e. ( 0 ..^ N ) )
76	69 72 74 75	fourierdlem8	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) [,] ( S ` ( j + 1 ) ) ) C_ ( C [,] D ) )
77	67 76	sstrid	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) C_ ( C [,] D ) )
78	77	resabs1d	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
79	3	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> M e. NN )
80	4	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> Q e. ( P ` M ) )
81	5	adantr	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> F : RR --> CC )
82	6	adantlr	\|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
83	7	adantlr	\|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
84		eqid	\|- ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) = ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) )
85		eqid	\|- ( F \|` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) = ( F \|` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) )
86		eqid	\|- ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) \|-> ( ( F \|` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) ) = ( y e. ( ( ( J ` ( E ` ( S ` j ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) (,) ( ( E ` ( S ` ( j + 1 ) ) ) + ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) \|-> ( ( F \|` ( ( J ` ( E ` ( S ` j ) ) ) (,) ( E ` ( S ` ( j + 1 ) ) ) ) ) ` ( y - ( ( S ` ( j + 1 ) ) - ( E ` ( S ` ( j + 1 ) ) ) ) ) ) )
87	1 2 79 80 81 82 83 68 70 12 14 13 15 16 17 75 84 85 86 18	fourierdlem90	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
88	78 87	eqeltrd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) e. ( ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) -cn-> CC ) )
89	8	adantlr	\|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
90		eqid	\|- ( i e. ( 0 ..^ M ) \|-> R ) = ( i e. ( 0 ..^ M ) \|-> R )
91	1 2 79 80 81 82 83 89 68 70 12 14 13 15 16 17 75 84 18 90	fourierdlem89	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0 ..^ M ) \|-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
92	78	eqcomd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) = ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) )
93	92	oveq1d	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) = ( ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
94	91 93	eleqtrd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> if ( ( J ` ( E ` ( S ` j ) ) ) = ( Q ` ( I ` ( S ` j ) ) ) , ( ( i e. ( 0 ..^ M ) \|-> R ) ` ( I ` ( S ` j ) ) ) , ( F ` ( J ` ( E ` ( S ` j ) ) ) ) ) e. ( ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` j ) ) )
95	9	adantlr	\|- ( ( ( ph /\ j e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ M ) ) -> L e. ( ( F \|` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` ( i + 1 ) ) ) )
96		eqid	\|- ( i e. ( 0 ..^ M ) \|-> L ) = ( i e. ( 0 ..^ M ) \|-> L )
97	1 2 79 80 81 82 83 95 68 70 12 14 13 15 16 17 75 84 18 96	fourierdlem91	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> if ( ( E ` ( S ` ( j + 1 ) ) ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) , ( ( i e. ( 0 ..^ M ) \|-> L ) ` ( I ` ( S ` j ) ) ) , ( F ` ( E ` ( S ` ( j + 1 ) ) ) ) ) e. ( ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
98	92	oveq1d	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> ( ( F \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) = ( ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
99	97 98	eleqtrd	\|- ( ( ph /\ j e. ( 0 ..^ N ) ) -> if ( ( E ` ( S ` ( j + 1 ) ) ) = ( Q ` ( ( I ` ( S ` j ) ) + 1 ) ) , ( ( i e. ( 0 ..^ M ) \|-> L ) ` ( I ` ( S ` j ) ) ) , ( F ` ( E ` ( S ` ( j + 1 ) ) ) ) ) e. ( ( ( F \|` ( C [,] D ) ) \|` ( ( S ` j ) (,) ( S ` ( j + 1 ) ) ) ) limCC ( S ` ( j + 1 ) ) ) )
100	32 64 65 66 88 94 99	fourierdlem69	\|- ( ph -> ( F \|` ( C [,] D ) ) e. L^1 )
101	22 100	eqeltrrd	\|- ( ph -> ( x e. ( C [,] D ) \|-> ( F ` x ) ) e. L^1 )

Metamath Proof Explorer

Theorem fourierdlem100

Proof