Metamath Proof Explorer

Theorem itgsbtaddcnst

Description: Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsbtaddcnst.a 
|- ( ph -> A e. RR )
itgsbtaddcnst.b 
|- ( ph -> B e. RR )
itgsbtaddcnst.aleb 
|- ( ph -> A <_ B )
itgsbtaddcnst.x 
|- ( ph -> X e. RR )
itgsbtaddcnst.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
Assertion itgsbtaddcnst 
|- ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( F ` ( X + s ) ) _d s = S_ [ A -> B ] ( F ` t ) _d t )

Proof

Step Hyp Ref Expression
1 itgsbtaddcnst.a 
 |-  ( ph -> A e. RR )
2 itgsbtaddcnst.b 
 |-  ( ph -> B e. RR )
3 itgsbtaddcnst.aleb 
 |-  ( ph -> A <_ B )
4 itgsbtaddcnst.x 
 |-  ( ph -> X e. RR )
5 itgsbtaddcnst.f 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
6 1 2 iccssred 
 |-  ( ph -> ( A [,] B ) C_ RR )
7 6 sselda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. RR )
8 7 recnd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. CC )
9 4 recnd 
 |-  ( ph -> X e. CC )
10 9 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> X e. CC )
11 8 10 negsubd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t + -u X ) = ( t - X ) )
12 11 eqcomd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t - X ) = ( t + -u X ) )
13 12 mpteq2dva 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t - X ) ) = ( t e. ( A [,] B ) |-> ( t + -u X ) ) )
14 1 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> A e. RR )
15 4 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> X e. RR )
16 14 15 resubcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( A - X ) e. RR )
17 2 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> B e. RR )
18 17 15 resubcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( B - X ) e. RR )
19 7 15 resubcld 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t - X ) e. RR )
20 simpr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t e. ( A [,] B ) )
21 1 2 jca 
 |-  ( ph -> ( A e. RR /\ B e. RR ) )
22 21 adantr 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( A e. RR /\ B e. RR ) )
23 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( t e. ( A [,] B ) <-> ( t e. RR /\ A <_ t /\ t <_ B ) ) )
24 22 23 syl 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t e. ( A [,] B ) <-> ( t e. RR /\ A <_ t /\ t <_ B ) ) )
25 20 24 mpbid 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t e. RR /\ A <_ t /\ t <_ B ) )
26 25 simp2d 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> A <_ t )
27 14 7 15 26 lesub1dd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( A - X ) <_ ( t - X ) )
28 25 simp3d 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> t <_ B )
29 7 17 15 28 lesub1dd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t - X ) <_ ( B - X ) )
30 16 18 19 27 29 eliccd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t - X ) e. ( ( A - X ) [,] ( B - X ) ) )
31 30 fmpttd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t - X ) ) : ( A [,] B ) --> ( ( A - X ) [,] ( B - X ) ) )
32 13 31 feq1dd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t + -u X ) ) : ( A [,] B ) --> ( ( A - X ) [,] ( B - X ) ) )
33 1 4 resubcld 
 |-  ( ph -> ( A - X ) e. RR )
34 2 4 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
35 33 34 iccssred 
 |-  ( ph -> ( ( A - X ) [,] ( B - X ) ) C_ RR )
36 ax-resscn 
 |-  RR C_ CC
37 35 36 sstrdi 
 |-  ( ph -> ( ( A - X ) [,] ( B - X ) ) C_ CC )
38 6 36 sstrdi 
 |-  ( ph -> ( A [,] B ) C_ CC )
39 38 resmptd 
 |-  ( ph -> ( ( t e. CC |-> ( t - X ) ) |` ( A [,] B ) ) = ( t e. ( A [,] B ) |-> ( t - X ) ) )
40 ssid 
 |-  CC C_ CC
41 cncfmptid 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
42 40 40 41 mp2an 
 |-  ( t e. CC |-> t ) e. ( CC -cn-> CC )
43 42 a1i 
 |-  ( X e. CC -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
44 40 a1i 
 |-  ( X e. CC -> CC C_ CC )
45 id 
 |-  ( X e. CC -> X e. CC )
46 44 45 44 constcncfg 
 |-  ( X e. CC -> ( t e. CC |-> X ) e. ( CC -cn-> CC ) )
47 43 46 subcncf 
 |-  ( X e. CC -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
48 9 47 syl 
 |-  ( ph -> ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) )
49 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( ( t e. CC |-> ( t - X ) ) e. ( CC -cn-> CC ) -> ( ( t e. CC |-> ( t - X ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
50 38 48 49 sylc 
 |-  ( ph -> ( ( t e. CC |-> ( t - X ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
51 39 50 eqeltrrd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t - X ) ) e. ( ( A [,] B ) -cn-> CC ) )
52 13 51 eqeltrrd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t + -u X ) ) e. ( ( A [,] B ) -cn-> CC ) )
53 cncffvrn 
 |-  ( ( ( ( A - X ) [,] ( B - X ) ) C_ CC /\ ( t e. ( A [,] B ) |-> ( t + -u X ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( ( t e. ( A [,] B ) |-> ( t + -u X ) ) e. ( ( A [,] B ) -cn-> ( ( A - X ) [,] ( B - X ) ) ) <-> ( t e. ( A [,] B ) |-> ( t + -u X ) ) : ( A [,] B ) --> ( ( A - X ) [,] ( B - X ) ) ) )
54 37 52 53 syl2anc 
 |-  ( ph -> ( ( t e. ( A [,] B ) |-> ( t + -u X ) ) e. ( ( A [,] B ) -cn-> ( ( A - X ) [,] ( B - X ) ) ) <-> ( t e. ( A [,] B ) |-> ( t + -u X ) ) : ( A [,] B ) --> ( ( A - X ) [,] ( B - X ) ) ) )
55 32 54 mpbird 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t + -u X ) ) e. ( ( A [,] B ) -cn-> ( ( A - X ) [,] ( B - X ) ) ) )
56 13 55 eqeltrd 
 |-  ( ph -> ( t e. ( A [,] B ) |-> ( t - X ) ) e. ( ( A [,] B ) -cn-> ( ( A - X ) [,] ( B - X ) ) ) )
57 eqid 
 |-  ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( X + s ) )
58 9 adantr 
 |-  ( ( ph /\ s e. CC ) -> X e. CC )
59 simpr 
 |-  ( ( ph /\ s e. CC ) -> s e. CC )
60 58 59 addcomd 
 |-  ( ( ph /\ s e. CC ) -> ( X + s ) = ( s + X ) )
61 60 mpteq2dva 
 |-  ( ph -> ( s e. CC |-> ( X + s ) ) = ( s e. CC |-> ( s + X ) ) )
62 eqid 
 |-  ( s e. CC |-> ( s + X ) ) = ( s e. CC |-> ( s + X ) )
63 62 addccncf 
 |-  ( X e. CC -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
64 9 63 syl 
 |-  ( ph -> ( s e. CC |-> ( s + X ) ) e. ( CC -cn-> CC ) )
65 61 64 eqeltrd 
 |-  ( ph -> ( s e. CC |-> ( X + s ) ) e. ( CC -cn-> CC ) )
66 1 adantr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> A e. RR )
67 2 adantr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> B e. RR )
68 4 adantr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> X e. RR )
69 35 sselda 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> s e. RR )
70 68 69 readdcld 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + s ) e. RR )
71 simpr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> s e. ( ( A - X ) [,] ( B - X ) ) )
72 33 adantr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) e. RR )
73 34 adantr 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( B - X ) e. RR )
74 elicc2 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR ) -> ( s e. ( ( A - X ) [,] ( B - X ) ) <-> ( s e. RR /\ ( A - X ) <_ s /\ s <_ ( B - X ) ) ) )
75 72 73 74 syl2anc 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( s e. ( ( A - X ) [,] ( B - X ) ) <-> ( s e. RR /\ ( A - X ) <_ s /\ s <_ ( B - X ) ) ) )
76 71 75 mpbid 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( s e. RR /\ ( A - X ) <_ s /\ s <_ ( B - X ) ) )
77 76 simp2d 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) <_ s )
78 66 68 69 lesubadd2d 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( A - X ) <_ s <-> A <_ ( X + s ) ) )
79 77 78 mpbid 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> A <_ ( X + s ) )
80 76 simp3d 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> s <_ ( B - X ) )
81 68 69 67 leaddsub2d 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( X + s ) <_ B <-> s <_ ( B - X ) ) )
82 80 81 mpbird 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + s ) <_ B )
83 66 67 70 79 82 eliccd 
 |-  ( ( ph /\ s e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + s ) e. ( A [,] B ) )
84 57 65 37 38 83 cncfmptssg 
 |-  ( ph -> ( s e. ( ( A - X ) [,] ( B - X ) ) |-> ( X + s ) ) e. ( ( ( A - X ) [,] ( B - X ) ) -cn-> ( A [,] B ) ) )
85 84 5 cncfcompt 
 |-  ( ph -> ( s e. ( ( A - X ) [,] ( B - X ) ) |-> ( F ` ( X + s ) ) ) e. ( ( ( A - X ) [,] ( B - X ) ) -cn-> CC ) )
86 ax-1cn 
 |-  1 e. CC
87 ioosscn 
 |-  ( A (,) B ) C_ CC
88 cncfmptc 
 |-  ( ( 1 e. CC /\ ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( t e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
89 86 87 40 88 mp3an 
 |-  ( t e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC )
90 89 a1i 
 |-  ( ph -> ( t e. ( A (,) B ) |-> 1 ) e. ( ( A (,) B ) -cn-> CC ) )
91 fconstmpt 
 |-  ( ( A (,) B ) X. { 1 } ) = ( t e. ( A (,) B ) |-> 1 )
92 ioombl 
 |-  ( A (,) B ) e. dom vol
93 92 a1i 
 |-  ( ph -> ( A (,) B ) e. dom vol )
94 volioo 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol ` ( A (,) B ) ) = ( B - A ) )
95 1 2 3 94 syl3anc 
 |-  ( ph -> ( vol ` ( A (,) B ) ) = ( B - A ) )
96 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
97 95 96 eqeltrd 
 |-  ( ph -> ( vol ` ( A (,) B ) ) e. RR )
98 1cnd 
 |-  ( ph -> 1 e. CC )
99 iblconst 
 |-  ( ( ( A (,) B ) e. dom vol /\ ( vol ` ( A (,) B ) ) e. RR /\ 1 e. CC ) -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
100 93 97 98 99 syl3anc 
 |-  ( ph -> ( ( A (,) B ) X. { 1 } ) e. L^1 )
101 91 100 eqeltrrid 
 |-  ( ph -> ( t e. ( A (,) B ) |-> 1 ) e. L^1 )
102 90 101 elind 
 |-  ( ph -> ( t e. ( A (,) B ) |-> 1 ) e. ( ( ( A (,) B ) -cn-> CC ) i^i L^1 ) )
103 36 a1i 
 |-  ( ph -> RR C_ CC )
104 19 recnd 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( t - X ) e. CC )
105 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
106 105 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
107 iccntr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
108 21 107 syl 
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( A [,] B ) ) = ( A (,) B ) )
109 103 6 104 106 105 108 dvmptntr 
 |-  ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t - X ) ) ) = ( RR _D ( t e. ( A (,) B ) |-> ( t - X ) ) ) )
110 reelprrecn 
 |-  RR e. { RR , CC }
111 110 a1i 
 |-  ( ph -> RR e. { RR , CC } )
112 ioossre 
 |-  ( A (,) B ) C_ RR
113 112 sseli 
 |-  ( t e. ( A (,) B ) -> t e. RR )
114 113 adantl 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. RR )
115 114 recnd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. CC )
116 1cnd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> 1 e. CC )
117 103 sselda 
 |-  ( ( ph /\ t e. RR ) -> t e. CC )
118 1cnd 
 |-  ( ( ph /\ t e. RR ) -> 1 e. CC )
119 111 dvmptid 
 |-  ( ph -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
120 112 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
121 iooretop 
 |-  ( A (,) B ) e. ( topGen ` ran (,) )
122 121 a1i 
 |-  ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
123 111 117 118 119 120 106 105 122 dvmptres 
 |-  ( ph -> ( RR _D ( t e. ( A (,) B ) |-> t ) ) = ( t e. ( A (,) B ) |-> 1 ) )
124 9 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> X e. CC )
125 0cnd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> 0 e. CC )
126 9 adantr 
 |-  ( ( ph /\ t e. RR ) -> X e. CC )
127 0cnd 
 |-  ( ( ph /\ t e. RR ) -> 0 e. CC )
128 111 9 dvmptc 
 |-  ( ph -> ( RR _D ( t e. RR |-> X ) ) = ( t e. RR |-> 0 ) )
129 111 126 127 128 120 106 105 122 dvmptres 
 |-  ( ph -> ( RR _D ( t e. ( A (,) B ) |-> X ) ) = ( t e. ( A (,) B ) |-> 0 ) )
130 111 115 116 123 124 125 129 dvmptsub 
 |-  ( ph -> ( RR _D ( t e. ( A (,) B ) |-> ( t - X ) ) ) = ( t e. ( A (,) B ) |-> ( 1 - 0 ) ) )
131 116 subid1d 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( 1 - 0 ) = 1 )
132 131 mpteq2dva 
 |-  ( ph -> ( t e. ( A (,) B ) |-> ( 1 - 0 ) ) = ( t e. ( A (,) B ) |-> 1 ) )
133 109 130 132 3eqtrd 
 |-  ( ph -> ( RR _D ( t e. ( A [,] B ) |-> ( t - X ) ) ) = ( t e. ( A (,) B ) |-> 1 ) )
134 oveq2 
 |-  ( s = ( t - X ) -> ( X + s ) = ( X + ( t - X ) ) )
135 134 fveq2d 
 |-  ( s = ( t - X ) -> ( F ` ( X + s ) ) = ( F ` ( X + ( t - X ) ) ) )
136 oveq1 
 |-  ( t = A -> ( t - X ) = ( A - X ) )
137 oveq1 
 |-  ( t = B -> ( t - X ) = ( B - X ) )
138 1 2 3 56 85 102 133 135 136 137 33 34 itgsubsticc 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( F ` ( X + s ) ) _d s = S_ [ A -> B ] ( ( F ` ( X + ( t - X ) ) ) x. 1 ) _d t )
139 124 115 pncan3d 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( X + ( t - X ) ) = t )
140 139 fveq2d 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( F ` ( X + ( t - X ) ) ) = ( F ` t ) )
141 140 oveq1d 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( F ` ( X + ( t - X ) ) ) x. 1 ) = ( ( F ` t ) x. 1 ) )
142 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> CC ) -> F : ( A [,] B ) --> CC )
143 5 142 syl 
 |-  ( ph -> F : ( A [,] B ) --> CC )
144 143 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> F : ( A [,] B ) --> CC )
145 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
146 145 sseli 
 |-  ( t e. ( A (,) B ) -> t e. ( A [,] B ) )
147 146 adantl 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. ( A [,] B ) )
148 144 147 ffvelrnd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( F ` t ) e. CC )
149 148 mulid1d 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( F ` t ) x. 1 ) = ( F ` t ) )
150 141 149 eqtrd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( ( F ` ( X + ( t - X ) ) ) x. 1 ) = ( F ` t ) )
151 3 150 ditgeq3d 
 |-  ( ph -> S_ [ A -> B ] ( ( F ` ( X + ( t - X ) ) ) x. 1 ) _d t = S_ [ A -> B ] ( F ` t ) _d t )
152 138 151 eqtrd 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( F ` ( X + s ) ) _d s = S_ [ A -> B ] ( F ` t ) _d t )