This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem97

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem97.f 
|- ( ph -> F : RR --> RR )
fourierdlem97.g 
|- G = ( RR _D F )
fourierdlem97.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 ) ) ) } )
fourierdlem97.a 
|- ( ph -> B e. RR )
fourierdlem97.b 
|- ( ph -> A e. RR )
fourierdlem97.t 
|- T = ( B - A )
fourierdlem97.m 
|- ( ph -> M e. NN )
fourierdlem97.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem97.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem97.qcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem97.c 
|- ( ph -> C e. RR )
fourierdlem97.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem97.j 
|- ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
fourierdlem97.v 
|- V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
fourierdlem97.h 
|- H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )
Assertion fourierdlem97 
|- ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 fourierdlem97.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem97.g 
 |-  G = ( RR _D F )
3 fourierdlem97.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 ) ) ) } )
4 fourierdlem97.a 
 |-  ( ph -> B e. RR )
5 fourierdlem97.b 
 |-  ( ph -> A e. RR )
6 fourierdlem97.t 
 |-  T = ( B - A )
7 fourierdlem97.m 
 |-  ( ph -> M e. NN )
8 fourierdlem97.q 
 |-  ( ph -> Q e. ( P ` M ) )
9 fourierdlem97.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
10 fourierdlem97.qcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
11 fourierdlem97.c 
 |-  ( ph -> C e. RR )
12 fourierdlem97.d 
 |-  ( ph -> D e. ( C (,) +oo ) )
13 fourierdlem97.j 
 |-  ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
14 fourierdlem97.v 
 |-  V = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
15 fourierdlem97.h 
 |-  H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) )
16 ioossre 
 |-  ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR
17 16 a1i 
 |-  ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ RR )
18 17 sselda 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. RR )
19 iftrue 
 |-  ( s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
20 19 adantl 
 |-  ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
21 ssid 
 |-  RR C_ RR
22 dvfre 
 |-  ( ( F : RR --> RR /\ RR C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
23 1 21 22 sylancl 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
24 2 feq1i 
 |-  ( G : dom ( RR _D F ) --> RR <-> ( RR _D F ) : dom ( RR _D F ) --> RR )
25 23 24 sylibr 
 |-  ( ph -> G : dom ( RR _D F ) --> RR )
26 25 adantr 
 |-  ( ( ph /\ s e. dom G ) -> G : dom ( RR _D F ) --> RR )
27 id 
 |-  ( s e. dom G -> s e. dom G )
28 2 dmeqi 
 |-  dom G = dom ( RR _D F )
29 27 28 eleqtrdi 
 |-  ( s e. dom G -> s e. dom ( RR _D F ) )
30 29 adantl 
 |-  ( ( ph /\ s e. dom G ) -> s e. dom ( RR _D F ) )
31 26 30 ffvelcdmd 
 |-  ( ( ph /\ s e. dom G ) -> ( G ` s ) e. RR )
32 20 31 eqeltrd 
 |-  ( ( ph /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
33 32 adantlr 
 |-  ( ( ( ph /\ s e. RR ) /\ s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
34 iffalse 
 |-  ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
35 0red 
 |-  ( -. s e. dom G -> 0 e. RR )
36 34 35 eqeltrd 
 |-  ( -. s e. dom G -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
37 36 adantl 
 |-  ( ( ( ph /\ s e. RR ) /\ -. s e. dom G ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
38 33 37 pm2.61dan 
 |-  ( ( ph /\ s e. RR ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
39 18 38 syldan 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
40 15 fvmpt2 
 |-  ( ( s e. RR /\ if ( s e. dom G , ( G ` s ) , 0 ) e. RR ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
41 18 39 40 syl2anc 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
42 elioore 
 |-  ( D e. ( C (,) +oo ) -> D e. RR )
43 12 42 syl 
 |-  ( ph -> D e. RR )
44 11 rexrd 
 |-  ( ph -> C e. RR* )
45 pnfxr 
 |-  +oo e. RR*
46 45 a1i 
 |-  ( ph -> +oo e. RR* )
47 ioogtlb 
 |-  ( ( C e. RR* /\ +oo e. RR* /\ D e. ( C (,) +oo ) ) -> C < D )
48 44 46 12 47 syl3anc 
 |-  ( ph -> C < D )
49 oveq1 
 |-  ( y = x -> ( y + ( h x. T ) ) = ( x + ( h x. T ) ) )
50 49 eleq1d 
 |-  ( y = x -> ( ( y + ( h x. T ) ) e. ran Q <-> ( x + ( h x. T ) ) e. ran Q ) )
51 50 rexbidv 
 |-  ( y = x -> ( E. h e. ZZ ( y + ( h x. T ) ) e. ran Q <-> E. h e. ZZ ( x + ( h x. T ) ) e. ran Q ) )
52 51 cbvrabv 
 |-  { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } = { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q }
53 52 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) = ( { C , D } u. { x e. ( C [,] D ) | E. h e. ZZ ( x + ( h x. T ) ) e. ran Q } )
54 oveq1 
 |-  ( k = l -> ( k x. T ) = ( l x. T ) )
55 54 oveq2d 
 |-  ( k = l -> ( y + ( k x. T ) ) = ( y + ( l x. T ) ) )
56 55 eleq1d 
 |-  ( k = l -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
57 56 cbvrexvw 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q )
58 57 a1i 
 |-  ( y e. ( C [,] D ) -> ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
59 58 rabbiia 
 |-  { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
60 59 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. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
61 oveq1 
 |-  ( l = h -> ( l x. T ) = ( h x. T ) )
62 61 oveq2d 
 |-  ( l = h -> ( y + ( l x. T ) ) = ( y + ( h x. T ) ) )
63 62 eleq1d 
 |-  ( l = h -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
64 63 cbvrexvw 
 |-  ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
65 64 a1i 
 |-  ( y e. ( C [,] D ) -> ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q ) )
66 65 rabbiia 
 |-  { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q }
67 66 uneq2i 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
68 60 67 eqtri 
 |-  ( { 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. h e. ZZ ( y + ( h x. T ) ) e. ran Q } )
69 68 fveq2i 
 |-  ( # ` ( { 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. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) )
70 69 oveq1i 
 |-  ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) - 1 )
71 oveq1 
 |-  ( k = h -> ( k x. T ) = ( h x. T ) )
72 71 oveq2d 
 |-  ( k = h -> ( ( Q ` 0 ) + ( k x. T ) ) = ( ( Q ` 0 ) + ( h x. T ) ) )
73 72 breq1d 
 |-  ( k = h -> ( ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) <-> ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) ) )
74 73 cbvrabv 
 |-  { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } = { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) }
75 74 supeq1i 
 |-  sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { h e. ZZ | ( ( Q ` 0 ) + ( h x. T ) ) <_ ( V ` J ) } , RR , < )
76 fveq2 
 |-  ( j = e -> ( Q ` j ) = ( Q ` e ) )
77 76 oveq1d 
 |-  ( j = e -> ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) = ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) )
78 77 breq1d 
 |-  ( j = e -> ( ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) <-> ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) ) )
79 78 cbvrabv 
 |-  { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } = { e e. ( 0 ..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) }
80 79 supeq1i 
 |-  sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) = sup ( { e e. ( 0 ..^ M ) | ( ( Q ` e ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < )
81 6 3 7 8 11 43 48 53 70 14 13 75 80 fourierdlem64 
 |-  ( ph -> ( ( sup ( { j e. ( 0 ..^ M ) | ( ( Q ` j ) + ( sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) x. T ) ) <_ ( V ` J ) } , RR , < ) e. ( 0 ..^ M ) /\ sup ( { k e. ZZ | ( ( Q ` 0 ) + ( k x. T ) ) <_ ( V ` J ) } , RR , < ) e. ZZ ) /\ E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) )
82 81 simprd 
 |-  ( ph -> E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
83 simpl1 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ph )
84 simpl2l 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> i e. ( 0 ..^ M ) )
85 cncff 
 |-  ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
86 10 85 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC )
87 ffun 
 |-  ( G : dom ( RR _D F ) --> RR -> Fun G )
88 25 87 syl 
 |-  ( ph -> Fun G )
89 88 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Fun G )
90 ffvresb 
 |-  ( Fun G -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
91 89 90 syl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) : ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) --> CC <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) ) )
92 86 91 mpbid 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ( s e. dom G /\ ( G ` s ) e. CC ) )
93 92 r19.21bi 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( s e. dom G /\ ( G ` s ) e. CC ) )
94 93 simpld 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. dom G )
95 94 ralrimiva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
96 dfss3 
 |-  ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G <-> A. s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) s e. dom G )
97 95 96 sylibr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
98 83 84 97 syl2anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ dom G )
99 simpl2 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( i e. ( 0 ..^ M ) /\ l e. ZZ ) )
100 83 99 jca 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) )
101 simpl3 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
102 simpr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) )
103 101 102 sseldd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
104 3 fourierdlem2 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
105 7 104 syl 
 |-  ( ph -> ( Q e. ( P ` M ) <-> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )
106 8 105 mpbid 
 |-  ( ph -> ( Q e. ( RR ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = A /\ ( Q ` M ) = B ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
107 106 simpld 
 |-  ( ph -> Q e. ( RR ^m ( 0 ... M ) ) )
108 elmapi 
 |-  ( Q e. ( RR ^m ( 0 ... M ) ) -> Q : ( 0 ... M ) --> RR )
109 107 108 syl 
 |-  ( ph -> Q : ( 0 ... M ) --> RR )
110 109 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> Q : ( 0 ... M ) --> RR )
111 elfzofz 
 |-  ( i e. ( 0 ..^ M ) -> i e. ( 0 ... M ) )
112 111 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
113 110 112 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR )
114 113 rexrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` i ) e. RR* )
115 114 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR* )
116 115 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR* )
117 fzofzp1 
 |-  ( i e. ( 0 ..^ M ) -> ( i + 1 ) e. ( 0 ... M ) )
118 117 adantl 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( i + 1 ) e. ( 0 ... M ) )
119 110 118 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( Q ` ( i + 1 ) ) e. RR )
120 119 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` ( i + 1 ) ) e. RR )
121 120 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR )
122 121 rexrd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` ( i + 1 ) ) e. RR* )
123 elioore 
 |-  ( t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> t e. RR )
124 123 adantl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. RR )
125 zre 
 |-  ( l e. ZZ -> l e. RR )
126 125 adantl 
 |-  ( ( i e. ( 0 ..^ M ) /\ l e. ZZ ) -> l e. RR )
127 126 ad2antlr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> l e. RR )
128 4 5 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
129 6 128 eqeltrid 
 |-  ( ph -> T e. RR )
130 129 ad2antrr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> T e. RR )
131 127 130 remulcld 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( l x. T ) e. RR )
132 124 131 resubcld 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. RR )
133 113 adantrr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( Q ` i ) e. RR )
134 125 ad2antll 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> l e. RR )
135 129 adantr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> T e. RR )
136 134 135 remulcld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( l x. T ) e. RR )
137 133 136 readdcld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR )
138 137 rexrd 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
139 138 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) e. RR* )
140 120 136 readdcld 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR )
141 140 rexrd 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
142 141 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* )
143 simpr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
144 ioogtlb 
 |-  ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
145 139 142 143 144 syl3anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( Q ` i ) + ( l x. T ) ) < t )
146 133 adantr 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) e. RR )
147 146 131 124 ltaddsubd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( ( Q ` i ) + ( l x. T ) ) < t <-> ( Q ` i ) < ( t - ( l x. T ) ) ) )
148 145 147 mpbid 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( Q ` i ) < ( t - ( l x. T ) ) )
149 iooltub 
 |-  ( ( ( ( Q ` i ) + ( l x. T ) ) e. RR* /\ ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) e. RR* /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
150 139 142 143 149 syl3anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) )
151 124 131 121 ltsubaddd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) <-> t < ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) )
152 150 151 mpbird 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) < ( Q ` ( i + 1 ) ) )
153 116 122 132 148 152 eliood 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
154 100 103 153 syl2anc 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) )
155 98 154 sseldd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( t - ( l x. T ) ) e. dom G )
156 elioore 
 |-  ( t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -> t e. RR )
157 recn 
 |-  ( t e. RR -> t e. CC )
158 157 adantl 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t e. CC )
159 zcn 
 |-  ( l e. ZZ -> l e. CC )
160 159 ad2antlr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> l e. CC )
161 129 recnd 
 |-  ( ph -> T e. CC )
162 161 ad2antrr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> T e. CC )
163 160 162 mulcld 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( l x. T ) e. CC )
164 158 163 npcand 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) = t )
165 164 eqcomd 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
166 165 adantr 
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
167 ovex 
 |-  ( t - ( l x. T ) ) e. _V
168 eleq1 
 |-  ( s = ( t - ( l x. T ) ) -> ( s e. dom G <-> ( t - ( l x. T ) ) e. dom G ) )
169 168 anbi2d 
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) <-> ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) ) )
170 oveq1 
 |-  ( s = ( t - ( l x. T ) ) -> ( s + ( l x. T ) ) = ( ( t - ( l x. T ) ) + ( l x. T ) ) )
171 170 eleq1d 
 |-  ( s = ( t - ( l x. T ) ) -> ( ( s + ( l x. T ) ) e. dom G <-> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G ) )
172 170 fveq2d 
 |-  ( s = ( t - ( l x. T ) ) -> ( G ` ( s + ( l x. T ) ) ) = ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) )
173 fveq2 
 |-  ( s = ( t - ( l x. T ) ) -> ( G ` s ) = ( G ` ( t - ( l x. T ) ) ) )
174 172 173 eqeq12d 
 |-  ( s = ( t - ( l x. T ) ) -> ( ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) <-> ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
175 171 174 anbi12d 
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) <-> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) )
176 169 175 imbi12d 
 |-  ( s = ( t - ( l x. T ) ) -> ( ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) ) <-> ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) ) ) )
177 ax-resscn 
 |-  RR C_ CC
178 177 a1i 
 |-  ( ph -> RR C_ CC )
179 1 178 fssd 
 |-  ( ph -> F : RR --> CC )
180 179 adantr 
 |-  ( ( ph /\ l e. ZZ ) -> F : RR --> CC )
181 125 adantl 
 |-  ( ( ph /\ l e. ZZ ) -> l e. RR )
182 129 adantr 
 |-  ( ( ph /\ l e. ZZ ) -> T e. RR )
183 181 182 remulcld 
 |-  ( ( ph /\ l e. ZZ ) -> ( l x. T ) e. RR )
184 179 ad2antrr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> F : RR --> CC )
185 129 ad2antrr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> T e. RR )
186 simplr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> l e. ZZ )
187 simpr 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> s e. RR )
188 9 ad4ant14 
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
189 184 185 186 187 188 fperiodmul 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. RR ) -> ( F ` ( s + ( l x. T ) ) ) = ( F ` s ) )
190 180 183 189 2 fperdvper 
 |-  ( ( ( ph /\ l e. ZZ ) /\ s e. dom G ) -> ( ( s + ( l x. T ) ) e. dom G /\ ( G ` ( s + ( l x. T ) ) ) = ( G ` s ) ) )
191 167 176 190 vtocl 
 |-  ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G /\ ( G ` ( ( t - ( l x. T ) ) + ( l x. T ) ) ) = ( G ` ( t - ( l x. T ) ) ) ) )
192 191 simpld 
 |-  ( ( ( ph /\ l e. ZZ ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
193 192 adantlr 
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> ( ( t - ( l x. T ) ) + ( l x. T ) ) e. dom G )
194 166 193 eqeltrd 
 |-  ( ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) /\ ( t - ( l x. T ) ) e. dom G ) -> t e. dom G )
195 194 ex 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. RR ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
196 156 195 sylan2 
 |-  ( ( ( ph /\ l e. ZZ ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
197 196 adantlrl 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
198 197 3adantl3 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( ( t - ( l x. T ) ) e. dom G -> t e. dom G ) )
199 155 198 mpd 
 |-  ( ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) /\ t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> t e. dom G )
200 199 ralrimiva 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
201 dfss3 
 |-  ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G <-> A. t e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) t e. dom G )
202 200 201 sylibr 
 |-  ( ( ph /\ ( i e. ( 0 ..^ M ) /\ l e. ZZ ) /\ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
203 202 3exp 
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) /\ l e. ZZ ) -> ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) ) )
204 203 rexlimdvv 
 |-  ( ph -> ( E. i e. ( 0 ..^ M ) E. l e. ZZ ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ ( ( ( Q ` i ) + ( l x. T ) ) (,) ( ( Q ` ( i + 1 ) ) + ( l x. T ) ) ) -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G ) )
205 82 204 mpd 
 |-  ( ph -> ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) C_ dom G )
206 205 sselda 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> s e. dom G )
207 206 iftrued 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
208 41 207 eqtr2d 
 |-  ( ( ph /\ s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) -> ( G ` s ) = ( H ` s ) )
209 208 mpteq2dva 
 |-  ( ph -> ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
210 28 a1i 
 |-  ( ph -> dom G = dom ( RR _D F ) )
211 210 feq2d 
 |-  ( ph -> ( G : dom G --> RR <-> G : dom ( RR _D F ) --> RR ) )
212 25 211 mpbird 
 |-  ( ph -> G : dom G --> RR )
213 212 205 feqresmpt 
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( G ` s ) ) )
214 38 15 fmptd 
 |-  ( ph -> H : RR --> RR )
215 214 17 feqresmpt 
 |-  ( ph -> ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( s e. ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) |-> ( H ` s ) ) )
216 209 213 215 3eqtr4d 
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) = ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) )
217 214 178 fssd 
 |-  ( ph -> H : RR --> CC )
218 15 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
219 eleq1 
 |-  ( s = ( x + T ) -> ( s e. dom G <-> ( x + T ) e. dom G ) )
220 fveq2 
 |-  ( s = ( x + T ) -> ( G ` s ) = ( G ` ( x + T ) ) )
221 219 220 ifbieq1d 
 |-  ( s = ( x + T ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
222 179 129 9 2 fperdvper 
 |-  ( ( ph /\ x e. dom G ) -> ( ( x + T ) e. dom G /\ ( G ` ( x + T ) ) = ( G ` x ) ) )
223 222 simpld 
 |-  ( ( ph /\ x e. dom G ) -> ( x + T ) e. dom G )
224 223 iftrued 
 |-  ( ( ph /\ x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = ( G ` ( x + T ) ) )
225 221 224 sylan9eqr 
 |-  ( ( ( ph /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
226 225 adantllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` ( x + T ) ) )
227 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
228 129 adantr 
 |-  ( ( ph /\ x e. RR ) -> T e. RR )
229 227 228 readdcld 
 |-  ( ( ph /\ x e. RR ) -> ( x + T ) e. RR )
230 229 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. RR )
231 212 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> G : dom G --> RR )
232 223 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( x + T ) e. dom G )
233 231 232 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) e. RR )
234 218 226 230 233 fvmptd 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( G ` ( x + T ) ) )
235 222 simprd 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
236 235 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` ( x + T ) ) = ( G ` x ) )
237 eleq1 
 |-  ( s = x -> ( s e. dom G <-> x e. dom G ) )
238 fveq2 
 |-  ( s = x -> ( G ` s ) = ( G ` x ) )
239 237 238 ifbieq1d 
 |-  ( s = x -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
240 239 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( x e. dom G , ( G ` x ) , 0 ) )
241 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. RR )
242 simpr 
 |-  ( ( ph /\ x e. dom G ) -> x e. dom G )
243 242 iftrued 
 |-  ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
244 212 ffvelcdmda 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) e. RR )
245 243 244 eqeltrd 
 |-  ( ( ph /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
246 245 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) e. RR )
247 218 240 241 246 fvmptd 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` x ) = if ( x e. dom G , ( G ` x ) , 0 ) )
248 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> x e. dom G )
249 248 iftrued 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = ( G ` x ) )
250 247 249 eqtr2d 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( G ` x ) = ( H ` x ) )
251 234 236 250 3eqtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
252 229 recnd 
 |-  ( ( ph /\ x e. RR ) -> ( x + T ) e. CC )
253 228 recnd 
 |-  ( ( ph /\ x e. RR ) -> T e. CC )
254 252 253 negsubd 
 |-  ( ( ph /\ x e. RR ) -> ( ( x + T ) + -u T ) = ( ( x + T ) - T ) )
255 227 recnd 
 |-  ( ( ph /\ x e. RR ) -> x e. CC )
256 255 253 pncand 
 |-  ( ( ph /\ x e. RR ) -> ( ( x + T ) - T ) = x )
257 254 256 eqtr2d 
 |-  ( ( ph /\ x e. RR ) -> x = ( ( x + T ) + -u T ) )
258 257 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x = ( ( x + T ) + -u T ) )
259 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( x + T ) e. dom G )
260 simpll 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ph )
261 260 259 jca 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ph /\ ( x + T ) e. dom G ) )
262 eleq1 
 |-  ( y = ( x + T ) -> ( y e. dom G <-> ( x + T ) e. dom G ) )
263 262 anbi2d 
 |-  ( y = ( x + T ) -> ( ( ph /\ y e. dom G ) <-> ( ph /\ ( x + T ) e. dom G ) ) )
264 oveq1 
 |-  ( y = ( x + T ) -> ( y + -u T ) = ( ( x + T ) + -u T ) )
265 264 eleq1d 
 |-  ( y = ( x + T ) -> ( ( y + -u T ) e. dom G <-> ( ( x + T ) + -u T ) e. dom G ) )
266 264 fveq2d 
 |-  ( y = ( x + T ) -> ( G ` ( y + -u T ) ) = ( G ` ( ( x + T ) + -u T ) ) )
267 fveq2 
 |-  ( y = ( x + T ) -> ( G ` y ) = ( G ` ( x + T ) ) )
268 266 267 eqeq12d 
 |-  ( y = ( x + T ) -> ( ( G ` ( y + -u T ) ) = ( G ` y ) <-> ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
269 265 268 anbi12d 
 |-  ( y = ( x + T ) -> ( ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) <-> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
270 263 269 imbi12d 
 |-  ( y = ( x + T ) -> ( ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) ) <-> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) ) )
271 129 renegcld 
 |-  ( ph -> -u T e. RR )
272 161 mulm1d 
 |-  ( ph -> ( -u 1 x. T ) = -u T )
273 272 eqcomd 
 |-  ( ph -> -u T = ( -u 1 x. T ) )
274 273 adantr 
 |-  ( ( ph /\ y e. RR ) -> -u T = ( -u 1 x. T ) )
275 274 oveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( y + -u T ) = ( y + ( -u 1 x. T ) ) )
276 275 fveq2d 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` ( y + ( -u 1 x. T ) ) ) )
277 179 adantr 
 |-  ( ( ph /\ y e. RR ) -> F : RR --> CC )
278 129 adantr 
 |-  ( ( ph /\ y e. RR ) -> T e. RR )
279 1zzd 
 |-  ( ( ph /\ y e. RR ) -> 1 e. ZZ )
280 279 znegcld 
 |-  ( ( ph /\ y e. RR ) -> -u 1 e. ZZ )
281 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
282 9 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
283 277 278 280 281 282 fperiodmul 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + ( -u 1 x. T ) ) ) = ( F ` y ) )
284 276 283 eqtrd 
 |-  ( ( ph /\ y e. RR ) -> ( F ` ( y + -u T ) ) = ( F ` y ) )
285 179 271 284 2 fperdvper 
 |-  ( ( ph /\ y e. dom G ) -> ( ( y + -u T ) e. dom G /\ ( G ` ( y + -u T ) ) = ( G ` y ) ) )
286 270 285 vtoclg 
 |-  ( ( x + T ) e. dom G -> ( ( ph /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) ) )
287 259 261 286 sylc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( ( x + T ) + -u T ) e. dom G /\ ( G ` ( ( x + T ) + -u T ) ) = ( G ` ( x + T ) ) ) )
288 287 simpld 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> ( ( x + T ) + -u T ) e. dom G )
289 258 288 eqeltrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x + T ) e. dom G ) -> x e. dom G )
290 289 stoic1a 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. ( x + T ) e. dom G )
291 290 iffalsed 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) = 0 )
292 15 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> H = ( s e. RR |-> if ( s e. dom G , ( G ` s ) , 0 ) ) )
293 221 adantl 
 |-  ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = ( x + T ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
294 229 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( x + T ) e. RR )
295 0red 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> 0 e. RR )
296 291 295 eqeltrd 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) e. RR )
297 292 293 294 296 fvmptd 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = if ( ( x + T ) e. dom G , ( G ` ( x + T ) ) , 0 ) )
298 simpr 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> -. x e. dom G )
299 298 iffalsed 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> if ( x e. dom G , ( G ` x ) , 0 ) = 0 )
300 239 299 sylan9eqr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) /\ s = x ) -> if ( s e. dom G , ( G ` s ) , 0 ) = 0 )
301 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> x e. RR )
302 292 300 301 295 fvmptd 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` x ) = 0 )
303 291 297 302 3eqtr4d 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. dom G ) -> ( H ` ( x + T ) ) = ( H ` x ) )
304 251 303 pm2.61dan 
 |-  ( ( ph /\ x e. RR ) -> ( H ` ( x + T ) ) = ( H ` x ) )
305 elioore 
 |-  ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -> s e. RR )
306 305 adantl 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> s e. RR )
307 305 38 sylan2 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) e. RR )
308 306 307 40 syl2anc 
 |-  ( ( ph /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
309 308 adantlr 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = if ( s e. dom G , ( G ` s ) , 0 ) )
310 94 iftrued 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> if ( s e. dom G , ( G ` s ) , 0 ) = ( G ` s ) )
311 309 310 eqtrd 
 |-  ( ( ( ph /\ i e. ( 0 ..^ M ) ) /\ s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) -> ( H ` s ) = ( G ` s ) )
312 311 mpteq2dva 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
313 214 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> H : RR --> RR )
314 ioossre 
 |-  ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR
315 314 a1i 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) C_ RR )
316 313 315 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( H ` s ) ) )
317 212 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> G : dom G --> RR )
318 317 97 feqresmpt 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( s e. ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) |-> ( G ` s ) ) )
319 312 316 318 3eqtr4d 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) = ( G |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) )
320 319 10 eqeltrd 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( H |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
321 eqid 
 |-  ( 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. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
322 oveq1 
 |-  ( z = y -> ( z + ( l x. T ) ) = ( y + ( l x. T ) ) )
323 322 eleq1d 
 |-  ( z = y -> ( ( z + ( l x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
324 323 rexbidv 
 |-  ( z = y -> ( E. l e. ZZ ( z + ( l x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q ) )
325 324 cbvrabv 
 |-  { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } = { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q }
326 325 uneq2i 
 |-  ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } )
327 326 eqcomi 
 |-  ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { z e. ( C [,] D ) | E. l e. ZZ ( z + ( l x. T ) ) e. ran Q } )
328 60 fveq2i 
 |-  ( # ` ( { 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. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) )
329 328 oveq1i 
 |-  ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) = ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) - 1 )
330 isoeq5 
 |-  ( ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) = ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) -> ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) ) )
331 67 330 ax-mp 
 |-  ( g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
332 331 iotabii 
 |-  ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. h e. ZZ ( y + ( h x. T ) ) e. ran Q } ) ) )
333 isoeq1 
 |-  ( f = g -> ( f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) <-> g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) )
334 333 cbviotavw 
 |-  ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) ) = ( iota g g Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) )
335 332 334 14 3eqtr4ri 
 |-  V = ( iota f f Isom < , < ( ( 0 ... ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) , ( { C , D } u. { y e. ( C [,] D ) | E. l e. ZZ ( y + ( l x. T ) ) e. ran Q } ) ) )
336 id 
 |-  ( v = x -> v = x )
337 oveq2 
 |-  ( v = x -> ( B - v ) = ( B - x ) )
338 337 oveq1d 
 |-  ( v = x -> ( ( B - v ) / T ) = ( ( B - x ) / T ) )
339 338 fveq2d 
 |-  ( v = x -> ( |_ ` ( ( B - v ) / T ) ) = ( |_ ` ( ( B - x ) / T ) ) )
340 339 oveq1d 
 |-  ( v = x -> ( ( |_ ` ( ( B - v ) / T ) ) x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
341 336 340 oveq12d 
 |-  ( v = x -> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
342 341 cbvmptv 
 |-  ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
343 eqeq1 
 |-  ( u = z -> ( u = B <-> z = B ) )
344 id 
 |-  ( u = z -> u = z )
345 343 344 ifbieq2d 
 |-  ( u = z -> if ( u = B , A , u ) = if ( z = B , A , z ) )
346 345 cbvmptv 
 |-  ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) = ( z e. ( A (,] B ) |-> if ( z = B , A , z ) )
347 eqid 
 |-  ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) = ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) )
348 eqid 
 |-  ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) = ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) )
349 eqid 
 |-  ( z e. ( ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) (,) ( ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) |-> ( ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ` ( z - ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) ) = ( z e. ( ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) (,) ( ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) + ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) |-> ( ( H |` ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) (,) ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ` ( z - ( ( V ` ( J + 1 ) ) - ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` ( J + 1 ) ) ) ) ) ) )
350 fveq2 
 |-  ( i = t -> ( Q ` i ) = ( Q ` t ) )
351 350 breq1d 
 |-  ( i = t -> ( ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) <-> ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) ) )
352 351 cbvrabv 
 |-  { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } = { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) }
353 fveq2 
 |-  ( w = x -> ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) = ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) )
354 353 fveq2d 
 |-  ( w = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) )
355 354 eqcomd 
 |-  ( w = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) )
356 355 breq2d 
 |-  ( w = x -> ( ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) <-> ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) ) )
357 356 rabbidv 
 |-  ( w = x -> { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } = { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } )
358 352 357 eqtr2id 
 |-  ( w = x -> { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } )
359 358 supeq1d 
 |-  ( w = x -> sup ( { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } , RR , < ) = sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
360 359 cbvmptv 
 |-  ( w e. RR |-> sup ( { t e. ( 0 ..^ M ) | ( Q ` t ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` w ) ) } , RR , < ) ) = ( x e. RR |-> sup ( { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) } , RR , < ) )
361 3 6 7 8 217 304 320 11 12 321 327 329 335 342 346 13 347 348 349 360 fourierdlem90 
 |-  ( ph -> ( H |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )
362 216 361 eqeltrd 
 |-  ( ph -> ( G |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) e. ( ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) -cn-> CC ) )