Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem97 Structured version   Unicode version

Theorem fourierdlem97 31827
Description:  F is continuous on the intervals induced by the moved partition  V (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
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
Ref Expression
fourierdlem97  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  e.  ( ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) )
-cn-> CC ) )
Distinct variable groups:    A, i, x    A, m, p, i    B, i, x    B, m, p    y, C, g    C, i, x, y    C, m, p, y    y, D, g    D, i, x    D, m, p    F, s, x   
y, F    i, G, s    y, G    i, H, s, x    h, J, k, i, x    J, s   
h, M, i, x   
m, M, p    M, s    Q, h, k, g, y    Q, i, x    Q, m, p, k    Q, s    T, h, k, g, y    T, i, x    T, m, p    T, s    h, V, k, g    i, V, x    V, p    V, s    ph, h, y, g    ph, i,
s, x
Allowed substitution hints:    ph( k, m, p)    A( y, g, h, k, s)    B( y, g, h, k, s)    C( h, k, s)    D( h, k, s)    P( x, y, g, h, i, k, m, s, p)    F( g, h, i, k, m, p)    G( x, g, h, k, m, p)    H( y, g, h, k, m, p)    J( y,
g, m, p)    M( y, g, k)    V( y, m)

Proof of Theorem fourierdlem97
Dummy variables  f 
l  t  u  w  z  v  e  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem97.f . . . . . . 7  |-  ( ph  ->  F : RR --> RR )
2 ssid 3528 . . . . . . 7  |-  RR  C_  RR
3 dvfre 22222 . . . . . . 7  |-  ( ( F : RR --> RR  /\  RR  C_  RR )  -> 
( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
41, 2, 3sylancl 662 . . . . . 6  |-  ( ph  ->  ( RR  _D  F
) : dom  ( RR  _D  F ) --> RR )
5 fourierdlem97.g . . . . . . . 8  |-  G  =  ( RR  _D  F
)
65feq1i 5729 . . . . . . 7  |-  ( G : dom  ( RR 
_D  F ) --> RR  <->  ( RR  _D  F ) : dom  ( RR 
_D  F ) --> RR )
76a1i 11 . . . . . 6  |-  ( ph  ->  ( G : dom  ( RR  _D  F
) --> RR  <->  ( RR  _D  F ) : dom  ( RR  _D  F
) --> RR ) )
84, 7mpbird 232 . . . . 5  |-  ( ph  ->  G : dom  ( RR  _D  F ) --> RR )
95dmeqi 5210 . . . . . . 7  |-  dom  G  =  dom  ( RR  _D  F )
109a1i 11 . . . . . 6  |-  ( ph  ->  dom  G  =  dom  ( RR  _D  F
) )
1110feq2d 5724 . . . . 5  |-  ( ph  ->  ( G : dom  G --> RR  <->  G : dom  ( RR  _D  F ) --> RR ) )
128, 11mpbird 232 . . . 4  |-  ( ph  ->  G : dom  G --> RR )
13 fourierdlem97.t . . . . . . 7  |-  T  =  ( B  -  A
)
14 fourierdlem97.p . . . . . . 7  |-  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 ) ) ) } )
15 fourierdlem97.m . . . . . . 7  |-  ( ph  ->  M  e.  NN )
16 fourierdlem97.q . . . . . . 7  |-  ( ph  ->  Q  e.  ( P `
 M ) )
17 fourierdlem97.c . . . . . . 7  |-  ( ph  ->  C  e.  RR )
18 fourierdlem97.d . . . . . . . 8  |-  ( ph  ->  D  e.  ( C (,) +oo ) )
19 elioore 11571 . . . . . . . 8  |-  ( D  e.  ( C (,) +oo )  ->  D  e.  RR )
2018, 19syl 16 . . . . . . 7  |-  ( ph  ->  D  e.  RR )
2117rexrd 9655 . . . . . . . 8  |-  ( ph  ->  C  e.  RR* )
22 pnfxr 11333 . . . . . . . . 9  |- +oo  e.  RR*
2322a1i 11 . . . . . . . 8  |-  ( ph  -> +oo  e.  RR* )
24 ioogtlb 31415 . . . . . . . 8  |-  ( ( C  e.  RR*  /\ +oo  e.  RR*  /\  D  e.  ( C (,) +oo ) )  ->  C  <  D )
2521, 23, 18, 24syl3anc 1228 . . . . . . 7  |-  ( ph  ->  C  <  D )
26 oveq1 6302 . . . . . . . . . . 11  |-  ( y  =  x  ->  (
y  +  ( h  x.  T ) )  =  ( x  +  ( h  x.  T
) ) )
2726eleq1d 2536 . . . . . . . . . 10  |-  ( y  =  x  ->  (
( y  +  ( h  x.  T ) )  e.  ran  Q  <->  ( x  +  ( h  x.  T ) )  e.  ran  Q ) )
2827rexbidv 2978 . . . . . . . . 9  |-  ( y  =  x  ->  ( E. h  e.  ZZ  ( y  +  ( h  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  (
x  +  ( h  x.  T ) )  e.  ran  Q ) )
2928cbvrabv 3117 . . . . . . . 8  |-  { 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 }
3029uneq2i 3660 . . . . . . 7  |-  ( { 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 } )
31 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( k  =  l  ->  (
k  x.  T )  =  ( l  x.  T ) )
3231oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( k  =  l  ->  (
y  +  ( k  x.  T ) )  =  ( y  +  ( l  x.  T
) ) )
3332eleq1d 2536 . . . . . . . . . . . . . 14  |-  ( k  =  l  ->  (
( y  +  ( k  x.  T ) )  e.  ran  Q  <->  ( y  +  ( l  x.  T ) )  e.  ran  Q ) )
3433cbvrexv 3094 . . . . . . . . . . . . 13  |-  ( E. k  e.  ZZ  (
y  +  ( k  x.  T ) )  e.  ran  Q  <->  E. l  e.  ZZ  ( y  +  ( l  x.  T
) )  e.  ran  Q )
3534a1i 11 . . . . . . . . . . . 12  |-  ( 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 ) )
3635rabbiia 3107 . . . . . . . . . . 11  |-  { 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 }
3736uneq2i 3660 . . . . . . . . . 10  |-  ( { 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 } )
38 oveq1 6302 . . . . . . . . . . . . . . . 16  |-  ( l  =  h  ->  (
l  x.  T )  =  ( h  x.  T ) )
3938oveq2d 6311 . . . . . . . . . . . . . . 15  |-  ( l  =  h  ->  (
y  +  ( l  x.  T ) )  =  ( y  +  ( h  x.  T
) ) )
4039eleq1d 2536 . . . . . . . . . . . . . 14  |-  ( l  =  h  ->  (
( y  +  ( l  x.  T ) )  e.  ran  Q  <->  ( y  +  ( h  x.  T ) )  e.  ran  Q ) )
4140cbvrexv 3094 . . . . . . . . . . . . 13  |-  ( E. l  e.  ZZ  (
y  +  ( l  x.  T ) )  e.  ran  Q  <->  E. h  e.  ZZ  ( y  +  ( h  x.  T
) )  e.  ran  Q )
4241a1i 11 . . . . . . . . . . . 12  |-  ( 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 ) )
4342rabbiia 3107 . . . . . . . . . . 11  |-  { 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 }
4443uneq2i 3660 . . . . . . . . . 10  |-  ( { 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 } )
4537, 44eqtri 2496 . . . . . . . . 9  |-  ( { 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 } )
4645fveq2i 5875 . . . . . . . 8  |-  ( # `  ( { 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 } ) )
4746oveq1i 6305 . . . . . . 7  |-  ( (
# `  ( { 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 )
48 fourierdlem97.v . . . . . . 7  |-  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 }
) ) )
49 fourierdlem97.j . . . . . . 7  |-  ( ph  ->  J  e.  ( 0..^ ( ( # `  ( { C ,  D }  u.  { y  e.  ( C [,] D )  |  E. k  e.  ZZ  ( y  +  ( k  x.  T
) )  e.  ran  Q } ) )  - 
1 ) ) )
50 oveq1 6302 . . . . . . . . . . 11  |-  ( k  =  h  ->  (
k  x.  T )  =  ( h  x.  T ) )
5150oveq2d 6311 . . . . . . . . . 10  |-  ( k  =  h  ->  (
( Q `  0
)  +  ( k  x.  T ) )  =  ( ( Q `
 0 )  +  ( h  x.  T
) ) )
5251breq1d 4463 . . . . . . . . 9  |-  ( k  =  h  ->  (
( ( Q ` 
0 )  +  ( k  x.  T ) )  <_  ( V `  J )  <->  ( ( Q `  0 )  +  ( h  x.  T ) )  <_ 
( V `  J
) ) )
5352cbvrabv 3117 . . . . . . . 8  |-  { k  e.  ZZ  |  ( ( Q `  0
)  +  ( k  x.  T ) )  <_  ( V `  J ) }  =  { h  e.  ZZ  |  ( ( Q `
 0 )  +  ( h  x.  T
) )  <_  ( V `  J ) }
5453supeq1i 7919 . . . . . . 7  |-  sup ( { k  e.  ZZ  |  ( ( Q `
 0 )  +  ( k  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )  =  sup ( { h  e.  ZZ  |  ( ( Q `
 0 )  +  ( h  x.  T
) )  <_  ( V `  J ) } ,  RR ,  <  )
55 fveq2 5872 . . . . . . . . . . 11  |-  ( j  =  e  ->  ( Q `  j )  =  ( Q `  e ) )
5655oveq1d 6310 . . . . . . . . . 10  |-  ( 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
) ) )
5756breq1d 4463 . . . . . . . . 9  |-  ( 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
) ) )
5857cbvrabv 3117 . . . . . . . 8  |-  { 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
) }
5958supeq1i 7919 . . . . . . 7  |-  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 ,  <  )
6013, 14, 15, 16, 17, 20, 25, 30, 47, 48, 49, 54, 59fourierdlem64 31794 . . . . . 6  |-  ( 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
) ) ) ) )
6160simprd 463 . . . . 5  |-  ( 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 ) ) ) )
62 simpl1 999 . . . . . . . . . . . 12  |-  ( ( ( 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 )
63 simpl2l 1049 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
64 fourierdlem97.qcn . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
65 cncff 21265 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 )
6664, 65syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ) : ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) --> CC )
67 ffun 5739 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G : dom  ( RR 
_D  F ) --> RR 
->  Fun  G )
688, 67syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  Fun  G )
6968adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Fun  G )
70 ffvresb 6063 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) )
7169, 70syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) )
7266, 71mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( s  e.  dom  G  /\  ( G `  s )  e.  CC ) )
7372adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  A. s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) ( s  e. 
dom  G  /\  ( G `  s )  e.  CC ) )
74 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )
75 rspa 2834 . . . . . . . . . . . . . . . . 17  |-  ( ( A. s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ( s  e.  dom  G  /\  ( G `  s )  e.  CC )  /\  s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) )  ->  ( s  e.  dom  G  /\  ( G `  s )  e.  CC ) )
7673, 74, 75syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  (
s  e.  dom  G  /\  ( G `  s
)  e.  CC ) )
7776simpld 459 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  dom  G )
7877ralrimiva 2881 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  A. s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) s  e.  dom  G
)
79 dfss3 3499 . . . . . . . . . . . . . 14  |-  ( ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
C_  dom  G  <->  A. s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) s  e.  dom  G )
8078, 79sylibr 212 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
8180idi 2 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  dom  G )
8262, 63, 81syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( 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 )
83 simpl2 1000 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
)
8462, 83jca 532 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
85 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) )
86 simpl3 1001 . . . . . . . . . . . . 13  |-  ( ( ( 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
) ) ) )
87 simpr 461 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  /\  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  C_  (
( ( Q `  i )  +  ( l  x.  T ) ) (,) ( ( Q `  ( i  +  1 ) )  +  ( l  x.  T ) ) ) )
88 simpl 457 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  /\  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  t  e.  ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )
8987, 88sseldd 3510 . . . . . . . . . . . . 13  |-  ( ( t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  /\  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  t  e.  ( ( ( Q `  i )  +  ( l  x.  T ) ) (,) ( ( Q `  ( i  +  1 ) )  +  ( l  x.  T ) ) ) )
9085, 86, 89syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( 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
) ) ) )
9114fourierdlem2 31732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) ) ) )
9215, 91syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) ) )
9316, 92mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( Q  e.  ( RR  ^m  ( 0 ... M ) )  /\  ( ( ( Q `  0 )  =  A  /\  ( Q `  M )  =  B )  /\  A. i  e.  ( 0..^ M ) ( Q `
 i )  < 
( Q `  (
i  +  1 ) ) ) ) )
9493simpld 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  Q  e.  ( RR 
^m  ( 0 ... M ) ) )
95 elmapi 7452 . . . . . . . . . . . . . . . . . . 19  |-  ( Q  e.  ( RR  ^m  ( 0 ... M
) )  ->  Q : ( 0 ... M ) --> RR )
9694, 95syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  Q : ( 0 ... M ) --> RR )
9796adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  Q : ( 0 ... M ) --> RR )
98 elfzofz 11823 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 0..^ M )  ->  i  e.  ( 0 ... M
) )
9998adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  i  e.  ( 0 ... M ) )
10097, 99ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR )
101100rexrd 9655 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  i )  e.  RR* )
102101adantrr 716 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  i )  e.  RR* )
103102adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( 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* )
104 fzofzp1 11889 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( 0..^ M )  ->  ( i  +  1 )  e.  ( 0 ... M
) )
105104adantl 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( i  +  1 )  e.  ( 0 ... M ) )
10697, 105ffvelrnd 6033 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
107106adantrr 716 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  ( i  +  1 ) )  e.  RR )
108107adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
109108rexrd 9655 . . . . . . . . . . . . 13  |-  ( ( ( 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* )
110 elioore 11571 . . . . . . . . . . . . . . 15  |-  ( t  e.  ( ( ( Q `  i )  +  ( l  x.  T ) ) (,) ( ( Q `  ( i  +  1 ) )  +  ( l  x.  T ) ) )  ->  t  e.  RR )
111110adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  t  e.  RR )
112 zre 10880 . . . . . . . . . . . . . . . . 17  |-  ( l  e.  ZZ  ->  l  e.  RR )
113112adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ M )  /\  l  e.  ZZ )  ->  l  e.  RR )
114113ad2antlr 726 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  l  e.  RR )
11513a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  =  ( B  -  A ) )
116 fourierdlem97.a . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  B  e.  RR )
117 fourierdlem97.b . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A  e.  RR )
118116, 117resubcld 9999 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( B  -  A
)  e.  RR )
119115, 118eqeltrd 2555 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  RR )
120119ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  /\  t  e.  ( (
( Q `  i
)  +  ( l  x.  T ) ) (,) ( ( Q `
 ( i  +  1 ) )  +  ( l  x.  T
) ) ) )  ->  T  e.  RR )
121114, 120remulcld 9636 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
122111, 121resubcld 9999 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
123100adantrr 716 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  ( Q `  i )  e.  RR )
124112ad2antll 728 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  l  e.  RR )
125119adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  T  e.  RR )
126124, 125remulcld 9636 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
l  x.  T )  e.  RR )
127123, 126readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  i
)  +  ( l  x.  T ) )  e.  RR )
128127rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  i
)  +  ( l  x.  T ) )  e.  RR* )
129128adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( 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* )
130107, 126readdcld 9635 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  (
i  +  1 ) )  +  ( l  x.  T ) )  e.  RR )
131130rexrd 9655 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( i  e.  ( 0..^ M )  /\  l  e.  ZZ ) )  ->  (
( Q `  (
i  +  1 ) )  +  ( l  x.  T ) )  e.  RR* )
132131adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( 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* )
133 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
134 ioogtlb 31415 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 )
135129, 132, 133, 134syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( 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
)
136123adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
137136, 121, 111ltaddsubd 10164 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
138135, 137mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
139 iooltub 31435 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) ) )
140129, 132, 133, 139syl3anc 1228 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
141111, 121, 108ltsubaddd 10160 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
142140, 141mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
143103, 109, 122, 138, 142eliood 31418 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
14484, 90, 143syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) ) )
14582, 144sseldd 3510 . . . . . . . . . 10  |-  ( ( ( 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
)
146 simpl 457 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( ph  /\  l  e.  ZZ ) )
147 ioossre 11598 . . . . . . . . . . . . . . 15  |-  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  C_  RR
148147sseli 3505 . . . . . . . . . . . . . 14  |-  ( t  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  ->  t  e.  RR )
149148adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  t  e.  RR )
150 ax-resscn 9561 . . . . . . . . . . . . . . . . . . . 20  |-  RR  C_  CC
151150sseli 3505 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  RR  ->  t  e.  CC )
152151adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  t  e.  CC )
153150, 112sseldi 3507 . . . . . . . . . . . . . . . . . . . 20  |-  ( l  e.  ZZ  ->  l  e.  CC )
154153ad2antlr 726 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  l  e.  CC )
155119recnd 9634 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  CC )
156155ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  T  e.  CC )
157154, 156mulcld 9628 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
l  x.  T )  e.  CC )
158152, 157npcand 9946 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
( t  -  (
l  x.  T ) )  +  ( l  x.  T ) )  =  t )
159158eqcomd 2475 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  t  =  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) ) )
160159adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  t  =  ( ( t  -  ( l  x.  T
) )  +  ( l  x.  T ) ) )
161 ovex 6320 . . . . . . . . . . . . . . . . . 18  |-  ( t  -  ( l  x.  T ) )  e. 
_V
162 eleq1 2539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
s  e.  dom  G  <->  ( t  -  ( l  x.  T ) )  e.  dom  G ) )
163162anbi2d 703 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
( ( ph  /\  l  e.  ZZ )  /\  s  e.  dom  G )  <->  ( ( ph  /\  l  e.  ZZ )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G ) ) )
164 oveq1 6302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
s  +  ( l  x.  T ) )  =  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) ) )
165164eleq1d 2536 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  (
( s  +  ( l  x.  T ) )  e.  dom  G  <->  ( ( t  -  (
l  x.  T ) )  +  ( l  x.  T ) )  e.  dom  G ) )
166164fveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  ( G `  ( s  +  ( l  x.  T ) ) )  =  ( G `  ( ( t  -  ( l  x.  T
) )  +  ( l  x.  T ) ) ) )
167 fveq2 5872 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( t  -  ( l  x.  T
) )  ->  ( G `  s )  =  ( G `  ( t  -  (
l  x.  T ) ) ) )
168166, 167eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 ) ) ) ) )
169165, 168anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) ) ) )
170163, 169imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) ) ) )
171150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  RR  C_  CC )
1721, 171fssd 5746 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : RR --> CC )
173172adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  l  e.  ZZ )  ->  F : RR
--> CC )
174112adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  l  e.  ZZ )  ->  l  e.  RR )
175119adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  l  e.  ZZ )  ->  T  e.  RR )
176174, 175remulcld 9636 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  l  e.  ZZ )  ->  ( l  x.  T )  e.  RR )
177173adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  F : RR --> CC )
178175adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  T  e.  RR )
179 simplr 754 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  l  e.  ZZ )
180 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  s  e.  RR )
181 fourierdlem97.fper . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 ( x  +  T ) )  =  ( F `  x
) )
182181adant423 31330 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T
) )  =  ( F `  x ) )
183177, 178, 179, 180, 182fperiodmul 31404 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  RR )  ->  ( F `  ( s  +  ( l  x.  T ) ) )  =  ( F `  s ) )
184173, 176, 183, 5fperdvper 31571 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  s  e.  dom  G )  -> 
( ( s  +  ( l  x.  T
) )  e.  dom  G  /\  ( G `  ( s  +  ( l  x.  T ) ) )  =  ( G `  s ) ) )
185170, 184vtoclg 3176 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  -  ( l  x.  T ) )  e.  _V  ->  (
( ( 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 ) ) ) ) ) )
186161, 185ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) ) ) )
187186simpld 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  (
t  -  ( l  x.  T ) )  e.  dom  G )  ->  ( ( t  -  ( l  x.  T ) )  +  ( l  x.  T
) )  e.  dom  G )
188187adantlr 714 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  ( (
t  -  ( l  x.  T ) )  +  ( l  x.  T ) )  e. 
dom  G )
189160, 188eqeltrd 2555 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  /\  ( t  -  ( l  x.  T
) )  e.  dom  G )  ->  t  e.  dom  G )
190189ex 434 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  RR )  ->  (
( t  -  (
l  x.  T ) )  e.  dom  G  ->  t  e.  dom  G
) )
191146, 149, 190syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  l  e.  ZZ )  /\  t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  (
( t  -  (
l  x.  T ) )  e.  dom  G  ->  t  e.  dom  G
) )
192191adantlrl 719 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
1931923adantl3 1154 . . . . . . . . . 10  |-  ( ( ( 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 ) )
194145, 193mpd 15 . . . . . . . . 9  |-  ( ( ( 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
)
195194ralrimiva 2881 . . . . . . . 8  |-  ( (
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 )
196 dfss3 3499 . . . . . . . 8  |-  ( ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) 
C_  dom  G  <->  A. t  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) t  e.  dom  G )
197195, 196sylibr 212 . . . . . . 7  |-  ( (
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 )
1981973exp 1195 . . . . . 6  |-  ( 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 ) ) )
199198rexlimdvv 2965 . . . . 5  |-  ( 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 ) )
20061, 199mpd 15 . . . 4  |-  ( ph  ->  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  dom  G )
20112, 200feqresmpt 5928 . . 3  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( s  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  |->  ( G `
 s ) ) )
202147a1i 11 . . . . . . 7  |-  ( ph  ->  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) )  C_  RR )
203202sselda 3509 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  s  e.  RR )
204 iftrue 3951 . . . . . . . . . . 11  |-  ( s  e.  dom  G  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
205204adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
2068adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  dom  G )  ->  G : dom  ( RR  _D  F ) --> RR )
207 id 22 . . . . . . . . . . . . 13  |-  ( s  e.  dom  G  -> 
s  e.  dom  G
)
2089a1i 11 . . . . . . . . . . . . 13  |-  ( s  e.  dom  G  ->  dom  G  =  dom  ( RR  _D  F ) )
209207, 208eleqtrd 2557 . . . . . . . . . . . 12  |-  ( s  e.  dom  G  -> 
s  e.  dom  ( RR  _D  F ) )
210209adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  dom  G )  ->  s  e.  dom  ( RR  _D  F ) )
211206, 210ffvelrnd 6033 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  dom  G )  ->  ( G `  s )  e.  RR )
212205, 211eqeltrd 2555 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
213212adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR )  /\  s  e.  dom  G )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
214 iffalse 3954 . . . . . . . . . 10  |-  ( -.  s  e.  dom  G  ->  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 )  =  0 )
215 0re 9608 . . . . . . . . . . 11  |-  0  e.  RR
216215a1i 11 . . . . . . . . . 10  |-  ( -.  s  e.  dom  G  ->  0  e.  RR )
217214, 216eqeltrd 2555 . . . . . . . . 9  |-  ( -.  s  e.  dom  G  ->  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 )  e.  RR )
218217adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  RR )  /\  -.  s  e.  dom  G )  ->  if ( s  e.  dom  G , 
( G `  s
) ,  0 )  e.  RR )
219213, 218pm2.61dan 789 . . . . . . 7  |-  ( (
ph  /\  s  e.  RR )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
220203, 219syldan 470 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
221 fourierdlem97.h . . . . . . 7  |-  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) )
222221fvmpt2 5964 . . . . . 6  |-  ( ( s  e.  RR  /\  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )  ->  ( H `  s )  =  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) )
223203, 220, 222syl2anc 661 . . . . 5  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
224200sselda 3509 . . . . . 6  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  s  e.  dom  G )
225224iftrued 3953 . . . . 5  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
226 eqidd 2468 . . . . 5  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( G `  s )  =  ( G `  s ) )
227223, 225, 2263eqtrrd 2513 . . . 4  |-  ( (
ph  /\  s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) )  ->  ( G `  s )  =  ( H `  s ) )
228227mpteq2dva 4539 . . 3  |-  ( ph  ->  ( s  e.  ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) 
|->  ( G `  s
) )  =  ( s  e.  ( ( V `  J ) (,) ( V `  ( J  +  1
) ) )  |->  ( H `  s ) ) )
229219, 221fmptd 6056 . . . . 5  |-  ( ph  ->  H : RR --> RR )
230229, 202feqresmpt 5928 . . . 4  |-  ( ph  ->  ( H  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( s  e.  ( ( V `
 J ) (,) ( V `  ( J  +  1 ) ) )  |->  ( H `
 s ) ) )
231230eqcomd 2475 . . 3  |-  ( ph  ->  ( s  e.  ( ( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) 
|->  ( H `  s
) )  =  ( H  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) ) )
232201, 228, 2313eqtrd 2512 . 2  |-  ( ph  ->  ( G  |`  (
( V `  J
) (,) ( V `
 ( J  + 
1 ) ) ) )  =  ( H  |`  ( ( V `  J ) (,) ( V `  ( J  +  1 ) ) ) ) )
233229, 171fssd 5746 . . 3  |-  ( ph  ->  H : RR --> CC )
234221a1i 11 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G , 
( G `  s
) ,  0 ) ) )
235 eleq1 2539 . . . . . . . . . 10  |-  ( s  =  ( x  +  T )  ->  (
s  e.  dom  G  <->  ( x  +  T )  e.  dom  G ) )
236 fveq2 5872 . . . . . . . . . 10  |-  ( s  =  ( x  +  T )  ->  ( G `  s )  =  ( G `  ( x  +  T
) ) )
237 eqidd 2468 . . . . . . . . . 10  |-  ( s  =  ( x  +  T )  ->  0  =  0 )
238235, 236, 237ifeq123d 31337 . . . . . . . . 9  |-  ( s  =  ( x  +  T )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  if ( ( x  +  T
)  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 ) )
239238adantl 466 . . . . . . . 8  |-  ( ( ( ph  /\  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 ) )
240172, 119, 181, 5fperdvper 31571 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
( x  +  T
)  e.  dom  G  /\  ( G `  (
x  +  T ) )  =  ( G `
 x ) ) )
241240simpld 459 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  (
x  +  T )  e.  dom  G )
242241iftrued 3953 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
243242adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  s  =  ( x  +  T ) )  ->  if ( ( x  +  T )  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
244239, 243eqtrd 2508 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  dom  G )  /\  s  =  ( x  +  T ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
245244adantllr 718 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  /\  s  =  ( x  +  T
) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 ( x  +  T ) ) )
246 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
247119adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  RR )
248246, 247readdcld 9635 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  RR )
249248adantr 465 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( x  +  T
)  e.  RR )
25012ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  G : dom  G --> RR )
251241adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( x  +  T
)  e.  dom  G
)
252250, 251ffvelrnd 6033 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  (
x  +  T ) )  e.  RR )
253234, 245, 249, 252fvmptd 5962 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  (
x  +  T ) )  =  ( G `
 ( x  +  T ) ) )
254240simprd 463 . . . . . 6  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  ( x  +  T ) )  =  ( G `  x
) )
255254adantlr 714 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  (
x  +  T ) )  =  ( G `
 x ) )
256 eleq1 2539 . . . . . . . . 9  |-  ( s  =  x  ->  (
s  e.  dom  G  <->  x  e.  dom  G ) )
257 fveq2 5872 . . . . . . . . 9  |-  ( s  =  x  ->  ( G `  s )  =  ( G `  x ) )
258 eqidd 2468 . . . . . . . . 9  |-  ( s  =  x  ->  0  =  0 )
259256, 257, 258ifeq123d 31337 . . . . . . . 8  |-  ( s  =  x  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  if ( x  e.  dom  G ,  ( G `  x ) ,  0 ) )
260259adantl 466 . . . . . . 7  |-  ( ( ( ( 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 ) )
261246adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  x  e.  RR )
262 simpr 461 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  dom  G )  ->  x  e.  dom  G )
263262iftrued 3953 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  =  ( G `
 x ) )
26412ffvelrnda 6032 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  dom  G )  ->  ( G `  x )  e.  RR )
265263, 264eqeltrd 2555 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  e.  RR )
266265adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  e.  RR )
267234, 260, 261, 266fvmptd 5962 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  x
)  =  if ( x  e.  dom  G ,  ( G `  x ) ,  0 ) )
268 simpr 461 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  x  e.  dom  G )
269268iftrued 3953 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  =  ( G `
 x ) )
270 eqidd 2468 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  x
)  =  ( G `
 x ) )
271267, 269, 2703eqtrrd 2513 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( G `  x
)  =  ( H `
 x ) )
272253, 255, 2713eqtrd 2512 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  x  e.  dom  G )  -> 
( H `  (
x  +  T ) )  =  ( H `
 x ) )
273221a1i 11 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  H  =  ( s  e.  RR  |->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 ) ) )
274238adantl 466 . . . . . 6  |-  ( ( ( ( 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 ) )
275248adantr 465 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( x  +  T )  e.  RR )
276150, 248sseldi 3507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  ( x  +  T )  e.  CC )
277150, 247sseldi 3507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  T  e.  CC )
278276, 277negsubd 9948 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  +  T )  +  -u T )  =  ( ( x  +  T )  -  T
) )
279150, 246sseldi 3507 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
280279, 277pncand 9943 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  +  T )  -  T )  =  x )
281278, 280eqtr2d 2509 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  RR )  ->  x  =  ( ( x  +  T )  +  -u T ) )
282281adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  x  =  ( ( x  +  T
)  +  -u T
) )
283 simpr 461 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( x  +  T )  e.  dom  G )
284 simpll 753 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ph )
285284, 283jca 532 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ph  /\  ( x  +  T
)  e.  dom  G
) )
286 eleq1 2539 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  +  T )  ->  (
y  e.  dom  G  <->  ( x  +  T )  e.  dom  G ) )
287286anbi2d 703 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x  +  T )  ->  (
( ph  /\  y  e.  dom  G )  <->  ( ph  /\  ( x  +  T
)  e.  dom  G
) ) )
288 oveq1 6302 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  +  T )  ->  (
y  +  -u T
)  =  ( ( x  +  T )  +  -u T ) )
289288eleq1d 2536 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  +  T )  ->  (
( y  +  -u T )  e.  dom  G  <-> 
( ( x  +  T )  +  -u T )  e.  dom  G ) )
290288fveq2d 5876 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  +  T )  ->  ( G `  ( y  +  -u T ) )  =  ( G `  ( ( x  +  T )  +  -u T ) ) )
291 fveq2 5872 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( x  +  T )  ->  ( G `  y )  =  ( G `  ( x  +  T
) ) )
292290, 291eqeq12d 2489 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( x  +  T )  ->  (
( G `  (
y  +  -u T
) )  =  ( G `  y )  <-> 
( G `  (
( x  +  T
)  +  -u T
) )  =  ( G `  ( x  +  T ) ) ) )
293289, 292anbi12d 710 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) ) )
294287, 293imbi12d 320 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) ) )
295119renegcld 9998 . . . . . . . . . . . . . . 15  |-  ( ph  -> 
-u T  e.  RR )
296155mulm1d 10020 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( -u 1  x.  T )  =  -u T )
297296eqcomd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
-u T  =  (
-u 1  x.  T
) )
298297adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR )  ->  -u T  =  ( -u 1  x.  T ) )
299298oveq2d 6311 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  ( y  +  -u T )  =  ( y  +  (
-u 1  x.  T
) ) )
300299fveq2d 5876 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  + 
-u T ) )  =  ( F `  ( y  +  (
-u 1  x.  T
) ) ) )
301172adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  F : RR
--> CC )
302119adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  T  e.  RR )
303 1z 10906 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  ZZ
304303a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  RR )  ->  1  e.  ZZ )
305304znegcld 10980 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  -u 1  e.  ZZ )
306 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  RR )  ->  y  e.  RR )
307181adantlr 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  RR )  /\  x  e.  RR )  ->  ( F `  ( x  +  T ) )  =  ( F `  x
) )
308301, 302, 305, 306, 307fperiodmul 31404 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  +  ( -u 1  x.  T ) ) )  =  ( F `  y ) )
309300, 308eqtrd 2508 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 ( y  + 
-u T ) )  =  ( F `  y ) )
310172, 295, 309, 5fperdvper 31571 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  dom  G )  ->  (
( y  +  -u T )  e.  dom  G  /\  ( G `  ( y  +  -u T ) )  =  ( G `  y
) ) )
311294, 310vtoclg 3176 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) ) )
312283, 285, 311sylc 60 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ( ( x  +  T )  +  -u T )  e. 
dom  G  /\  ( G `  ( (
x  +  T )  +  -u T ) )  =  ( G `  ( x  +  T
) ) ) )
313312simpld 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  ( ( x  +  T )  + 
-u T )  e. 
dom  G )
314282, 313eqeltrd 2555 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
x  +  T )  e.  dom  G )  ->  x  e.  dom  G )
315314ex 434 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( x  +  T )  e.  dom  G  ->  x  e.  dom  G ) )
316315con3dimp 441 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  -.  ( x  +  T )  e.  dom  G )
317316iffalsed 3956 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G , 
( G `  (
x  +  T ) ) ,  0 )  =  0 )
318215a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  0  e.  RR )
319317, 318eqeltrd 2555 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( ( x  +  T )  e.  dom  G , 
( G `  (
x  +  T ) ) ,  0 )  e.  RR )
320273, 274, 275, 319fvmptd 5962 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  ( x  +  T
) )  =  if ( ( x  +  T )  e.  dom  G ,  ( G `  ( x  +  T
) ) ,  0 ) )
321259adantl 466 . . . . . . . 8  |-  ( ( ( ( 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 ) )
322 simpr 461 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  -.  x  e.  dom  G )
323322iffalsed 3956 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  if ( x  e.  dom  G , 
( G `  x
) ,  0 )  =  0 )
324323adantr 465 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  /\  s  =  x )  ->  if ( x  e.  dom  G ,  ( G `  x ) ,  0 )  =  0 )
325321, 324eqtrd 2508 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  /\  s  =  x )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  0 )
326246adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  x  e.  RR )
327273, 325, 326, 318fvmptd 5962 . . . . . 6  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  x )  =  0 )
328327eqcomd 2475 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  0  =  ( H `  x ) )
329320, 317, 3283eqtrd 2512 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  -.  x  e.  dom  G )  ->  ( H `  ( x  +  T
) )  =  ( H `  x ) )
330272, 329pm2.61dan 789 . . 3  |-  ( (
ph  /\  x  e.  RR )  ->  ( H `
 ( x  +  T ) )  =  ( H `  x
) )
331229adantr 465 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  H : RR --> RR )
332 ioossre 11598 . . . . . . 7  |-  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  C_  RR
333332a1i 11 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  C_  RR )
334331, 333feqresmpt 5928 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( H `  s ) ) )
335332sseli 3505 . . . . . . . . . 10  |-  ( s  e.  ( ( Q `
 i ) (,) ( Q `  (
i  +  1 ) ) )  ->  s  e.  RR )
336335adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  s  e.  RR )
337336, 219syldan 470 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  e.  RR )
338336, 337, 222syl2anc 661 . . . . . . . 8  |-  ( (
ph  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
339338adantlr 714 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  if ( s  e. 
dom  G ,  ( G `  s ) ,  0 ) )
34077iftrued 3953 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  if ( s  e.  dom  G ,  ( G `  s ) ,  0 )  =  ( G `
 s ) )
341 eqidd 2468 . . . . . . 7  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( G `  s )  =  ( G `  s ) )
342339, 340, 3413eqtrd 2512 . . . . . 6  |-  ( ( ( ph  /\  i  e.  ( 0..^ M ) )  /\  s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  ->  ( H `  s )  =  ( G `  s ) )
343342mpteq2dva 4539 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( H `  s ) )  =  ( s  e.  ( ( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) 
|->  ( G `  s
) ) )
34412adantr 465 . . . . . . 7  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  G : dom  G --> RR )
345344, 80feqresmpt 5928 . . . . . 6  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( G  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( G `  s ) ) )
346345eqcomd 2475 . . . . 5  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( s  e.  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) )  |->  ( G `  s ) )  =  ( G  |`  (
( Q `  i
) (,) ( Q `
 ( i  +  1 ) ) ) ) )
347334, 343, 3463eqtrd 2512 . . . 4  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  =  ( G  |`  ( ( Q `  i ) (,) ( Q `  (
i  +  1 ) ) ) ) )
348347, 64eqeltrd 2555 . . 3  |-  ( (
ph  /\  i  e.  ( 0..^ M ) )  ->  ( H  |`  ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) )  e.  ( ( ( Q `  i ) (,) ( Q `  ( i  +  1 ) ) ) -cn-> CC ) )
349 eqid 2467 . . 3  |-  ( 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 ) ) ) } )
350 oveq1 6302 . . . . . . . 8  |-  ( z  =  y  ->  (
z  +  ( l  x.  T ) )  =  ( y  +  ( l  x.  T
) ) )
351350eleq1d 2536 . . . . . . 7  |-  ( z  =  y  ->  (
( z  +  ( l  x.  T ) )  e.  ran  Q  <->  ( y  +  ( l  x.  T ) )  e.  ran  Q ) )
352351rexbidv 2978 . . . . . 6  |-  ( z  =  y  ->  ( E. l  e.  ZZ  ( z  +  ( l  x.  T ) )  e.  ran  Q  <->  E. l  e.  ZZ  (
y  +  ( l  x.  T ) )  e.  ran  Q ) )
353352cbvrabv 3117 . . . . 5  |-  { 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 }
354353uneq2i 3660 . . . 4  |-  ( { 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 } )
355354eqcomi 2480 . . 3  |-  ( { 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 } )
35637fveq2i 5875 . . . 4  |-  ( # `  ( { 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 } ) )
357356oveq1i 6305 . . 3  |-  ( (
# `  ( { 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 )
358 isoeq1 6214 . . . . 5  |-  ( 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  (