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	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝑋 [,] 𝑌 ) ↦ 𝐴 ) ‘ 𝑌 ) ∈ ( 𝐾 [,] 𝐿 ) )
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 𝑥 )