Metamath Proof Explorer

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