Metamath Proof Explorer

Theorem fourierdlem96

Description: limit for F at the lower bound of an interval for the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem96.f 
|- ( ph -> F : RR --> RR )
fourierdlem96.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 ) ) ) } )
fourierdlem96.t 
|- T = ( B - A )
fourierdlem96.m 
|- ( ph -> M e. NN )
fourierdlem96.q 
|- ( ph -> Q e. ( P ` M ) )
fourierdlem96.fper 
|- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
fourierdlem96.qcn 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
fourierdlem96.8 
|- ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
fourierdlem96.c 
|- ( ph -> C e. RR )
fourierdlem96.d 
|- ( ph -> D e. ( C (,) +oo ) )
fourierdlem96.j 
|- ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
fourierdlem96.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 } ) ) )
Assertion fourierdlem96 
|- ( ph -> if ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( ( i e. ( 0 ..^ M ) |-> R ) ` ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( F ` ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) ) ) e. ( ( F |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) limCC ( V ` J ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem96.f 
 |-  ( ph -> F : RR --> RR )
2 fourierdlem96.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 ) ) ) } )
3 fourierdlem96.t 
 |-  T = ( B - A )
4 fourierdlem96.m 
 |-  ( ph -> M e. NN )
5 fourierdlem96.q 
 |-  ( ph -> Q e. ( P ` M ) )
6 fourierdlem96.fper 
 |-  ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )
7 fourierdlem96.qcn 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) e. ( ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) -cn-> CC ) )
8 fourierdlem96.8 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> R e. ( ( F |` ( ( Q ` i ) (,) ( Q ` ( i + 1 ) ) ) ) limCC ( Q ` i ) ) )
9 fourierdlem96.c 
 |-  ( ph -> C e. RR )
10 fourierdlem96.d 
 |-  ( ph -> D e. ( C (,) +oo ) )
11 fourierdlem96.j 
 |-  ( ph -> J e. ( 0 ..^ ( ( # ` ( { C , D } u. { y e. ( C [,] D ) | E. k e. ZZ ( y + ( k x. T ) ) e. ran Q } ) ) - 1 ) ) )
12 fourierdlem96.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 } ) ) )
13 ax-resscn 
 |-  RR C_ CC
14 13 a1i 
 |-  ( ph -> RR C_ CC )
15 1 14 fssd 
 |-  ( ph -> F : RR --> CC )
16 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 ) ) ) } )
17 oveq1 
 |-  ( z = y -> ( z + ( l x. T ) ) = ( y + ( l x. T ) ) )
18 17 eleq1d 
 |-  ( z = y -> ( ( z + ( l x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
19 18 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 ) )
20 19 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 }
21 20 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 } )
22 21 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 } )
23 oveq1 
 |-  ( k = l -> ( k x. T ) = ( l x. T ) )
24 23 oveq2d 
 |-  ( k = l -> ( y + ( k x. T ) ) = ( y + ( l x. T ) ) )
25 24 eleq1d 
 |-  ( k = l -> ( ( y + ( k x. T ) ) e. ran Q <-> ( y + ( l x. T ) ) e. ran Q ) )
26 25 cbvrexvw 
 |-  ( E. k e. ZZ ( y + ( k x. T ) ) e. ran Q <-> E. l e. ZZ ( y + ( l x. T ) ) e. ran Q )
27 26 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 ) )
28 27 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 }
29 28 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 } )
30 29 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 } ) )
31 30 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 )
32 oveq1 
 |-  ( l = h -> ( l x. T ) = ( h x. T ) )
33 32 oveq2d 
 |-  ( l = h -> ( y + ( l x. T ) ) = ( y + ( h x. T ) ) )
34 33 eleq1d 
 |-  ( l = h -> ( ( y + ( l x. T ) ) e. ran Q <-> ( y + ( h x. T ) ) e. ran Q ) )
35 34 cbvrexvw 
 |-  ( E. l e. ZZ ( y + ( l x. T ) ) e. ran Q <-> E. h e. ZZ ( y + ( h x. T ) ) e. ran Q )
36 35 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 ) )
37 36 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 }
38 37 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 } )
39 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 } ) ) ) )
40 38 39 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 } ) ) )
41 40 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 } ) ) )
42 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 } ) ) ) )
43 42 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 } ) ) )
44 41 43 12 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 } ) ) )
45 id 
 |-  ( v = x -> v = x )
46 oveq2 
 |-  ( v = x -> ( B - v ) = ( B - x ) )
47 46 oveq1d 
 |-  ( v = x -> ( ( B - v ) / T ) = ( ( B - x ) / T ) )
48 47 fveq2d 
 |-  ( v = x -> ( |_ ` ( ( B - v ) / T ) ) = ( |_ ` ( ( B - x ) / T ) ) )
49 48 oveq1d 
 |-  ( v = x -> ( ( |_ ` ( ( B - v ) / T ) ) x. T ) = ( ( |_ ` ( ( B - x ) / T ) ) x. T ) )
50 45 49 oveq12d 
 |-  ( v = x -> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) = ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
51 50 cbvmptv 
 |-  ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) = ( x e. RR |-> ( x + ( ( |_ ` ( ( B - x ) / T ) ) x. T ) ) )
52 eqeq1 
 |-  ( u = z -> ( u = B <-> z = B ) )
53 id 
 |-  ( u = z -> u = z )
54 52 53 ifbieq2d 
 |-  ( u = z -> if ( u = B , A , u ) = if ( z = B , A , z ) )
55 54 cbvmptv 
 |-  ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) = ( z e. ( A (,] B ) |-> if ( z = B , A , z ) )
56 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 ) ) ) )
57 fveq2 
 |-  ( j = i -> ( Q ` j ) = ( Q ` i ) )
58 57 breq1d 
 |-  ( j = i -> ( ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) <-> ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) ) )
59 58 cbvrabv 
 |-  { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) }
60 fveq2 
 |-  ( y = x -> ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) = ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) )
61 60 fveq2d 
 |-  ( y = x -> ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) = ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) )
62 61 breq2d 
 |-  ( y = x -> ( ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) <-> ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` x ) ) ) )
63 62 rabbidv 
 |-  ( y = x -> { i e. ( 0 ..^ M ) | ( Q ` i ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { 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 ) ) } )
64 59 63 syl5eq 
 |-  ( y = x -> { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } = { 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 ) ) } )
65 64 supeq1d 
 |-  ( y = x -> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , 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 , < ) )
66 65 cbvmptv 
 |-  ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , 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 , < ) )
67 eqid 
 |-  ( i e. ( 0 ..^ M ) |-> R ) = ( i e. ( 0 ..^ M ) |-> R )
68 2 3 4 5 15 6 7 8 9 10 16 22 31 44 51 55 11 56 66 67 fourierdlem89 
 |-  ( ph -> if ( ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) = ( Q ` ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( ( i e. ( 0 ..^ M ) |-> R ) ` ( ( y e. RR |-> sup ( { j e. ( 0 ..^ M ) | ( Q ` j ) <_ ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` y ) ) } , RR , < ) ) ` ( V ` J ) ) ) , ( F ` ( ( u e. ( A (,] B ) |-> if ( u = B , A , u ) ) ` ( ( v e. RR |-> ( v + ( ( |_ ` ( ( B - v ) / T ) ) x. T ) ) ) ` ( V ` J ) ) ) ) ) e. ( ( F |` ( ( V ` J ) (,) ( V ` ( J + 1 ) ) ) ) limCC ( V ` J ) ) )