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 ⊢ φ → X ∈ ℝ
itgsubsticc.2 ⊢ φ → Y ∈ ℝ
itgsubsticc.3 ⊢ φ → X ≤ Y
itgsubsticc.4 ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶cn K L
itgsubsticc.5 ⊢ φ → u ∈ K L ⟼ C : K L ⟶cn ℂ
itgsubsticc.6 ⊢ φ → x ∈ X Y ⟼ B ∈ X Y ⟶cn ℂ ∩ 𝐿 1
itgsubsticc.7 ⊢ φ → dx ∈ X Y A d ℝ x = x ∈ X Y ⟼ B
itgsubsticc.8 ⊢ u = A → C = E
itgsubsticc.9 ⊢ x = X → A = K
itgsubsticc.10 ⊢ x = Y → A = L
itgsubsticc.11 ⊢ φ → K ∈ ℝ
itgsubsticc.12 ⊢ φ → L ∈ ℝ
Assertion itgsubsticc ⊢ φ → ∫ K L C du = ∫ X Y E ⁢ B dx

Proof

Step Hyp Ref Expression
1 itgsubsticc.1 ⊢ φ → X ∈ ℝ
2 itgsubsticc.2 ⊢ φ → Y ∈ ℝ
3 itgsubsticc.3 ⊢ φ → X ≤ Y
4 itgsubsticc.4 ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶cn K L
5 itgsubsticc.5 ⊢ φ → u ∈ K L ⟼ C : K L ⟶cn ℂ
6 itgsubsticc.6 ⊢ φ → x ∈ X Y ⟼ B ∈ X Y ⟶cn ℂ ∩ 𝐿 1
7 itgsubsticc.7 ⊢ φ → dx ∈ X Y A d ℝ x = x ∈ 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 ⊢ φ → K ∈ ℝ
12 itgsubsticc.12 ⊢ φ → L ∈ ℝ
13 eqid ⊢ u ∈ K L ⟼ C = u ∈ K L ⟼ C
14 eqid ⊢ u ∈ ℝ ⟼ if u ∈ K L u ∈ K L ⟼ C ⁡ u if u < K u ∈ K L ⟼ C ⁡ K u ∈ K L ⟼ C ⁡ L = u ∈ ℝ ⟼ if u ∈ K L u ∈ K L ⟼ C ⁡ u if u < K u ∈ K L ⟼ C ⁡ K u ∈ K L ⟼ C ⁡ L
15 eqidd ⊢ φ → x ∈ X Y ⟼ A = x ∈ X Y ⟼ A
16 10 adantl ⊢ φ ∧ x = Y → A = L
17 1 rexrd ⊢ φ → X ∈ ℝ *
18 2 rexrd ⊢ φ → Y ∈ ℝ *
19 ubicc2 ⊢ X ∈ ℝ * ∧ Y ∈ ℝ * ∧ X ≤ Y → Y ∈ X Y
20 17 18 3 19 syl3anc ⊢ φ → Y ∈ X Y
21 15 16 20 12 fvmptd ⊢ φ → x ∈ X Y ⟼ A ⁡ Y = L
22 cncff ⊢ x ∈ X Y ⟼ A : X Y ⟶cn K L → x ∈ X Y ⟼ A : X Y ⟶ K L
23 4 22 syl ⊢ φ → x ∈ X Y ⟼ A : X Y ⟶ K L
24 23 20 ffvelcdmd ⊢ φ → x ∈ X Y ⟼ A ⁡ Y ∈ K L
25 21 24 eqeltrrd ⊢ φ → L ∈ K L
26 elicc2 ⊢ K ∈ ℝ ∧ L ∈ ℝ → L ∈ K L ↔ L ∈ ℝ ∧ K ≤ L ∧ L ≤ L
27 11 12 26 syl2anc ⊢ φ → L ∈ K L ↔ L ∈ ℝ ∧ K ≤ L ∧ L ≤ L
28 25 27 mpbid ⊢ φ → L ∈ ℝ ∧ K ≤ L ∧ L ≤ L
29 28 simp2d ⊢ φ → K ≤ L
30 13 14 1 2 3 4 6 5 11 12 29 7 8 9 10 itgsubsticclem ⊢ φ → ∫ K L C du = ∫ X Y E ⁢ B dx