Metamath Proof Explorer

Theorem fourierdlem82

Description: Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem82.1 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) )
fourierdlem82.2 
|- ( ph -> A e. RR )
fourierdlem82.3 
|- ( ph -> B e. RR )
fourierdlem82.4 
|- ( ph -> A < B )
fourierdlem82.5 
|- ( ph -> F : ( A [,] B ) --> CC )
fourierdlem82.6 
|- ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
fourierdlem82.7 
|- ( ph -> L e. ( F limCC B ) )
fourierdlem82.8 
|- ( ph -> R e. ( F limCC A ) )
fourierdlem82.9 
|- ( ph -> X e. RR )
Assertion fourierdlem82 
|- ( ph -> S. ( A [,] B ) ( F ` t ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )

Proof

Step Hyp Ref Expression
1 fourierdlem82.1 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) )
2 fourierdlem82.2 
 |-  ( ph -> A e. RR )
3 fourierdlem82.3 
 |-  ( ph -> B e. RR )
4 fourierdlem82.4 
 |-  ( ph -> A < B )
5 fourierdlem82.5 
 |-  ( ph -> F : ( A [,] B ) --> CC )
6 fourierdlem82.6 
 |-  ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
7 fourierdlem82.7 
 |-  ( ph -> L e. ( F limCC B ) )
8 fourierdlem82.8 
 |-  ( ph -> R e. ( F limCC A ) )
9 fourierdlem82.9 
 |-  ( ph -> X e. RR )
10 2 3 4 ltled 
 |-  ( ph -> A <_ B )
11 2 3 9 10 lesub1dd 
 |-  ( ph -> ( A - X ) <_ ( B - X ) )
12 11 ditgpos 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t = S. ( ( A - X ) (,) ( B - X ) ) ( G ` ( X + t ) ) _d t )
13 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = R )
14 13 adantl 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = R )
15 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
16 15 adantl 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
17 14 16 eqtr4d 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
18 17 adantlr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
19 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) )
20 iftrue 
 |-  ( x = B -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = L )
21 19 20 sylan9eq 
 |-  ( ( -. x = A /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = L )
22 21 adantll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = L )
23 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
24 iftrue 
 |-  ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
25 23 24 sylan9eq 
 |-  ( ( -. x = A /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
26 25 adantll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
27 22 26 eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
28 iffalse 
 |-  ( -. x = B -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
29 28 adantl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
30 19 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) )
31 iffalse 
 |-  ( -. x = B -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
32 31 adantl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
33 23 ad2antlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
34 2 rexrd 
 |-  ( ph -> A e. RR* )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
36 3 rexrd 
 |-  ( ph -> B e. RR* )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
38 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
39 3 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
40 simpr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
41 eliccre 
 |-  ( ( A e. RR /\ B e. RR /\ x e. ( A [,] B ) ) -> x e. RR )
42 38 39 40 41 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
43 42 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. RR )
44 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A e. RR )
45 42 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x e. RR )
46 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
47 38 39 46 syl2anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
48 40 47 mpbid 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
49 48 simp2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
50 49 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A <_ x )
51 neqne 
 |-  ( -. x = A -> x =/= A )
52 51 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x =/= A )
53 44 45 50 52 leneltd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A < x )
54 53 adantr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A < x )
55 42 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x e. RR )
56 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> B e. RR )
57 48 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
58 57 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x <_ B )
59 nesym 
 |-  ( B =/= x <-> -. x = B )
60 59 bilanri 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> B =/= x )
61 55 56 58 60 leneltd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x < B )
62 61 adantlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x < B )
63 35 37 43 54 62 eliood 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
64 fvres 
 |-  ( x e. ( A (,) B ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
65 63 64 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
66 32 33 65 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
67 29 30 66 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
68 27 67 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
69 18 68 pm2.61dan 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
70 69 mpteq2dva 
 |-  ( ph -> ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) ) = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
71 1 70 eqtrid 
 |-  ( ph -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
72 71 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
73 eqeq1 
 |-  ( x = ( X + t ) -> ( x = A <-> ( X + t ) = A ) )
74 eqeq1 
 |-  ( x = ( X + t ) -> ( x = B <-> ( X + t ) = B ) )
75 fveq2 
 |-  ( x = ( X + t ) -> ( F ` x ) = ( F ` ( X + t ) ) )
76 74 75 ifbieq2d 
 |-  ( x = ( X + t ) -> if ( x = B , L , ( F ` x ) ) = if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) )
77 73 76 ifbieq2d 
 |-  ( x = ( X + t ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) )
78 2 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A e. RR )
79 simpr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t e. ( ( A - X ) (,) ( B - X ) ) )
80 2 9 resubcld 
 |-  ( ph -> ( A - X ) e. RR )
81 80 rexrd 
 |-  ( ph -> ( A - X ) e. RR* )
82 81 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A - X ) e. RR* )
83 3 9 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
84 83 rexrd 
 |-  ( ph -> ( B - X ) e. RR* )
85 84 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( B - X ) e. RR* )
86 elioo2 
 |-  ( ( ( A - X ) e. RR* /\ ( B - X ) e. RR* ) -> ( t e. ( ( A - X ) (,) ( B - X ) ) <-> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) ) )
87 82 85 86 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( t e. ( ( A - X ) (,) ( B - X ) ) <-> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) ) )
88 79 87 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) )
89 88 simp2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A - X ) < t )
90 9 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> X e. RR )
91 88 simp1d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t e. RR )
92 78 90 91 ltsubadd2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( ( A - X ) < t <-> A < ( X + t ) ) )
93 89 92 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A < ( X + t ) )
94 78 93 gtned 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) =/= A )
95 94 neneqd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> -. ( X + t ) = A )
96 95 iffalsed 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) = if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) )
97 90 91 readdcld 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. RR )
98 88 simp3d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t < ( B - X ) )
99 3 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> B e. RR )
100 90 91 99 ltaddsub2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( ( X + t ) < B <-> t < ( B - X ) ) )
101 98 100 mpbird 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) < B )
102 97 101 ltned 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) =/= B )
103 102 neneqd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> -. ( X + t ) = B )
104 103 iffalsed 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) = ( F ` ( X + t ) ) )
105 96 104 eqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) = ( F ` ( X + t ) ) )
106 77 105 sylan9eqr 
 |-  ( ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) /\ x = ( X + t ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` ( X + t ) ) )
107 78 97 93 ltled 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A <_ ( X + t ) )
108 97 99 101 ltled 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) <_ B )
109 78 99 97 107 108 eliccd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. ( A [,] B ) )
110 5 ffund 
 |-  ( ph -> Fun F )
111 110 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> Fun F )
112 5 fdmd 
 |-  ( ph -> dom F = ( A [,] B ) )
113 112 eqcomd 
 |-  ( ph -> ( A [,] B ) = dom F )
114 113 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A [,] B ) = dom F )
115 109 114 eleqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. dom F )
116 fvelrn 
 |-  ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
117 111 115 116 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( F ` ( X + t ) ) e. ran F )
118 72 106 109 117 fvmptd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( G ` ( X + t ) ) = ( F ` ( X + t ) ) )
119 118 itgeq2dv 
 |-  ( ph -> S. ( ( A - X ) (,) ( B - X ) ) ( G ` ( X + t ) ) _d t = S. ( ( A - X ) (,) ( B - X ) ) ( F ` ( X + t ) ) _d t )
120 5 frnd 
 |-  ( ph -> ran F C_ CC )
121 120 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ran F C_ CC )
122 110 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> Fun F )
123 2 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> A e. RR )
124 3 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> B e. RR )
125 9 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> X e. RR )
126 80 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) e. RR )
127 83 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( B - X ) e. RR )
128 simpr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. ( ( A - X ) [,] ( B - X ) ) )
129 eliccre 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. RR )
130 126 127 128 129 syl3anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. RR )
131 125 130 readdcld 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. RR )
132 elicc2 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR ) -> ( t e. ( ( A - X ) [,] ( B - X ) ) <-> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) ) )
133 126 127 132 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( t e. ( ( A - X ) [,] ( B - X ) ) <-> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) ) )
134 128 133 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) )
135 134 simp2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) <_ t )
136 123 125 130 lesubadd2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( A - X ) <_ t <-> A <_ ( X + t ) ) )
137 135 136 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> A <_ ( X + t ) )
138 134 simp3d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t <_ ( B - X ) )
139 125 130 124 leaddsub2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( X + t ) <_ B <-> t <_ ( B - X ) ) )
140 138 139 mpbird 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) <_ B )
141 123 124 131 137 140 eliccd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. ( A [,] B ) )
142 113 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A [,] B ) = dom F )
143 141 142 eleqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. dom F )
144 122 143 116 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` ( X + t ) ) e. ran F )
145 121 144 sseldd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` ( X + t ) ) e. CC )
146 80 83 145 itgioo 
 |-  ( ph -> S. ( ( A - X ) (,) ( B - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )
147 12 119 146 3eqtrrd 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t = S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t )
148 nfv 
 |-  F/ x ph
149 2 3 4 5 limcicciooub 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC B ) = ( F limCC B ) )
150 7 149 eleqtrrd 
 |-  ( ph -> L e. ( ( F |` ( A (,) B ) ) limCC B ) )
151 2 3 4 5 limciccioolb 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC A ) = ( F limCC A ) )
152 8 151 eleqtrrd 
 |-  ( ph -> R e. ( ( F |` ( A (,) B ) ) limCC A ) )
153 148 1 2 3 6 150 152 cncfiooicc 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
154 2 3 10 9 153 itgsbtaddcnst 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t = S_ [ A -> B ] ( G ` s ) _d s )
155 10 ditgpos 
 |-  ( ph -> S_ [ A -> B ] ( G ` s ) _d s = S. ( A (,) B ) ( G ` s ) _d s )
156 fveq2 
 |-  ( s = t -> ( G ` s ) = ( G ` t ) )
157 156 cbvitgv 
 |-  S. ( A (,) B ) ( G ` s ) _d s = S. ( A (,) B ) ( G ` t ) _d t
158 1 a1i 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) ) )
159 2 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A e. RR )
160 simplr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t e. ( A (,) B ) )
161 34 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A e. RR* )
162 36 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> B e. RR* )
163 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( t e. ( A (,) B ) <-> ( t e. RR /\ A < t /\ t < B ) ) )
164 161 162 163 syl2anc 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( t e. ( A (,) B ) <-> ( t e. RR /\ A < t /\ t < B ) ) )
165 160 164 mpbid 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( t e. RR /\ A < t /\ t < B ) )
166 165 simp2d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A < t )
167 simpr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x = t )
168 166 167 breqtrrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A < x )
169 159 168 gtned 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x =/= A )
170 169 neneqd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> -. x = A )
171 170 iffalsed 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) )
172 165 simp1d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t e. RR )
173 167 172 eqeltrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x e. RR )
174 165 simp3d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t < B )
175 167 174 eqbrtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x < B )
176 173 175 ltned 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x =/= B )
177 176 neneqd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> -. x = B )
178 177 iffalsed 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
179 167 160 eqeltrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x e. ( A (,) B ) )
180 179 64 syl 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
181 fveq2 
 |-  ( x = t -> ( F ` x ) = ( F ` t ) )
182 181 adantl 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( F ` x ) = ( F ` t ) )
183 180 182 eqtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` t ) )
184 171 178 183 3eqtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = ( F ` t ) )
185 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
186 simpr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. ( A (,) B ) )
187 185 186 sselid 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. ( A [,] B ) )
188 110 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> Fun F )
189 113 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( A [,] B ) = dom F )
190 187 189 eleqtrd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. dom F )
191 fvelrn 
 |-  ( ( Fun F /\ t e. dom F ) -> ( F ` t ) e. ran F )
192 188 190 191 syl2anc 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( F ` t ) e. ran F )
193 158 184 187 192 fvmptd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( G ` t ) = ( F ` t ) )
194 193 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) ( G ` t ) _d t = S. ( A (,) B ) ( F ` t ) _d t )
195 157 194 eqtrid 
 |-  ( ph -> S. ( A (,) B ) ( G ` s ) _d s = S. ( A (,) B ) ( F ` t ) _d t )
196 5 ffvelcdmda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( F ` t ) e. CC )
197 2 3 196 itgioo 
 |-  ( ph -> S. ( A (,) B ) ( F ` t ) _d t = S. ( A [,] B ) ( F ` t ) _d t )
198 155 195 197 3eqtrd 
 |-  ( ph -> S_ [ A -> B ] ( G ` s ) _d s = S. ( A [,] B ) ( F ` t ) _d t )
199 147 154 198 3eqtrrd 
 |-  ( ph -> S. ( A [,] B ) ( F ` t ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )