Metamath Proof Explorer

Theorem itgsubsticc

Description: Integration by u-substitution. The main difference with respect to itgsubst is that here we consider the range of A ( x ) to be in the closed interval ( K , L ) . If A ( x ) is a continuous, differentiable function from [ X , Y ] to ( Z , W ) , whose derivative is continuous and integrable, and C ( u ) is a continuous function on ( Z , W ) , then the integral of C ( u ) from K = A ( X ) to L = A ( Y ) is equal to the integral of C ( A ( x ) ) _D A ( x ) from X to Y . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsubsticc.1 
|- ( ph -> X e. RR )
itgsubsticc.2 
|- ( ph -> Y e. RR )
itgsubsticc.3 
|- ( ph -> X <_ Y )
itgsubsticc.4 
|- ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )
itgsubsticc.5 
|- ( ph -> ( u e. ( K [,] L ) |-> C ) e. ( ( K [,] L ) -cn-> CC ) )
itgsubsticc.6 
|- ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
itgsubsticc.7 
|- ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
itgsubsticc.8 
|- ( u = A -> C = E )
itgsubsticc.9 
|- ( x = X -> A = K )
itgsubsticc.10 
|- ( x = Y -> A = L )
itgsubsticc.11 
|- ( ph -> K e. RR )
itgsubsticc.12 
|- ( ph -> L e. RR )
Assertion itgsubsticc 
|- ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )

Proof

Step Hyp Ref Expression
1 itgsubsticc.1 
 |-  ( ph -> X e. RR )
2 itgsubsticc.2 
 |-  ( ph -> Y e. RR )
3 itgsubsticc.3 
 |-  ( ph -> X <_ Y )
4 itgsubsticc.4 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) )
5 itgsubsticc.5 
 |-  ( ph -> ( u e. ( K [,] L ) |-> C ) e. ( ( K [,] L ) -cn-> CC ) )
6 itgsubsticc.6 
 |-  ( ph -> ( x e. ( X (,) Y ) |-> B ) e. ( ( ( X (,) Y ) -cn-> CC ) i^i L^1 ) )
7 itgsubsticc.7 
 |-  ( ph -> ( RR _D ( x e. ( X [,] Y ) |-> A ) ) = ( x e. ( X (,) Y ) |-> B ) )
8 itgsubsticc.8 
 |-  ( u = A -> C = E )
9 itgsubsticc.9 
 |-  ( x = X -> A = K )
10 itgsubsticc.10 
 |-  ( x = Y -> A = L )
11 itgsubsticc.11 
 |-  ( ph -> K e. RR )
12 itgsubsticc.12 
 |-  ( ph -> L e. RR )
13 eqid 
 |-  ( u e. ( K [,] L ) |-> C ) = ( u e. ( K [,] L ) |-> C )
14 eqid 
 |-  ( u e. RR |-> if ( u e. ( K [,] L ) , ( ( u e. ( K [,] L ) |-> C ) ` u ) , if ( u < K , ( ( u e. ( K [,] L ) |-> C ) ` K ) , ( ( u e. ( K [,] L ) |-> C ) ` L ) ) ) ) = ( u e. RR |-> if ( u e. ( K [,] L ) , ( ( u e. ( K [,] L ) |-> C ) ` u ) , if ( u < K , ( ( u e. ( K [,] L ) |-> C ) ` K ) , ( ( u e. ( K [,] L ) |-> C ) ` L ) ) ) )
15 eqidd 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) = ( x e. ( X [,] Y ) |-> A ) )
16 10 adantl 
 |-  ( ( ph /\ x = Y ) -> A = L )
17 1 rexrd 
 |-  ( ph -> X e. RR* )
18 2 rexrd 
 |-  ( ph -> Y e. RR* )
19 ubicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
20 17 18 3 19 syl3anc 
 |-  ( ph -> Y e. ( X [,] Y ) )
21 15 16 20 12 fvmptd 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> A ) ` Y ) = L )
22 cncff 
 |-  ( ( x e. ( X [,] Y ) |-> A ) e. ( ( X [,] Y ) -cn-> ( K [,] L ) ) -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
23 4 22 syl 
 |-  ( ph -> ( x e. ( X [,] Y ) |-> A ) : ( X [,] Y ) --> ( K [,] L ) )
24 23 20 ffvelcdmd 
 |-  ( ph -> ( ( x e. ( X [,] Y ) |-> A ) ` Y ) e. ( K [,] L ) )
25 21 24 eqeltrrd 
 |-  ( ph -> L e. ( K [,] L ) )
26 elicc2 
 |-  ( ( K e. RR /\ L e. RR ) -> ( L e. ( K [,] L ) <-> ( L e. RR /\ K <_ L /\ L <_ L ) ) )
27 11 12 26 syl2anc 
 |-  ( ph -> ( L e. ( K [,] L ) <-> ( L e. RR /\ K <_ L /\ L <_ L ) ) )
28 25 27 mpbid 
 |-  ( ph -> ( L e. RR /\ K <_ L /\ L <_ L ) )
29 28 simp2d 
 |-  ( ph -> K <_ L )
30 13 14 1 2 3 4 6 5 11 12 29 7 8 9 10 itgsubsticclem 
 |-  ( ph -> S_ [ K -> L ] C _d u = S_ [ X -> Y ] ( E x. B ) _d x )