This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
itgsubsticc.2 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
itgsubsticc.3 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
itgsubsticc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) )
itgsubsticc.5 ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ∈ ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) )
itgsubsticc.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
itgsubsticc.7 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
itgsubsticc.8 ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
itgsubsticc.9 ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
itgsubsticc.10 ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
itgsubsticc.11 ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
itgsubsticc.12 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
Assertion itgsubsticc ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgsubsticc.1 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
2 itgsubsticc.2 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3 itgsubsticc.3 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
4 itgsubsticc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) )
5 itgsubsticc.5 ⊢ ( 𝜑 → ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ∈ ( ( 𝐾 [,] 𝐿 ) –cn→ ℂ ) )
6 itgsubsticc.6 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) ∈ ( ( ( 𝑋 (,) 𝑌 ) –cn→ ℂ ) ∩ 𝐿1 ) )
7 itgsubsticc.7 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑋 (,) 𝑌 ) ↦ 𝐵 ) )
8 itgsubsticc.8 ⊢ ( 𝑢 = 𝐴 → 𝐶 = 𝐸 )
9 itgsubsticc.9 ⊢ ( 𝑥 = 𝑋 → 𝐴 = 𝐾 )
10 itgsubsticc.10 ⊢ ( 𝑥 = 𝑌 → 𝐴 = 𝐿 )
11 itgsubsticc.11 ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
12 itgsubsticc.12 ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
13 eqid ⊢ ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) = ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 )
14 eqid ⊢ ( 𝑢 ∈ ℝ ↦ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝐾 ) , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝐿 ) ) ) ) = ( 𝑢 ∈ ℝ ↦ if ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝑢 ) , if ( 𝑢 < 𝐾 , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝐾 ) , ( ( 𝑢 ∈ ( 𝐾 [,] 𝐿 ) ↦ 𝐶 ) ‘ 𝐿 ) ) ) )
15 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) = ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) )
16 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝐴 = 𝐿 )
17 1 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
18 2 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
19 ubicc2 ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑌 ∈ ℝ* ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
20 17 18 3 19 syl3anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑋 [,] 𝑌 ) )
21 15 16 20 12 fvmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑌 ) = 𝐿 )
22 cncff ⊢ ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ∈ ( ( 𝑋 [,] 𝑌 ) –cn→ ( 𝐾 [,] 𝐿 ) ) → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
23 4 22 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) : ( 𝑋 [,] 𝑌 ) ⟶ ( 𝐾 [,] 𝐿 ) )
24 23 20 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑌 ) ∈ ( 𝐾 [,] 𝐿 ) )
25 21 24 eqeltrrd ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐾 [,] 𝐿 ) )
26 elicc2 ⊢ ( ( 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝐿 ∈ ( 𝐾 [,] 𝐿 ) ↔ ( 𝐿 ∈ ℝ ∧ 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝐿 ) ) )
27 11 12 26 syl2anc ⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐾 [,] 𝐿 ) ↔ ( 𝐿 ∈ ℝ ∧ 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝐿 ) ) )
28 25 27 mpbid ⊢ ( 𝜑 → ( 𝐿 ∈ ℝ ∧ 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ 𝐿 ) )
29 28 simp2d ⊢ ( 𝜑 → 𝐾 ≤ 𝐿 )
30 13 14 1 2 3 4 6 5 11 12 29 7 8 9 10 itgsubsticclem ⊢ ( 𝜑 → ⨜ [ 𝐾 → 𝐿 ] 𝐶 d 𝑢 = ⨜ [ 𝑋 → 𝑌 ] ( 𝐸 · 𝐵 ) d 𝑥 )