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

Metamath Proof Explorer

Theorem itgmpt

Description: Change bound variable in an integral. (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypothesis itgmpt.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion itgmpt ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 )

Proof

Step Hyp Ref Expression
1 itgmpt.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
3 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 )
4 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 )
5 2 3 4 cbvitg ⊢ ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥
6 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
7 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
8 7 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
9 6 1 8 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
10 9 itgeq2dv ⊢ ( 𝜑 → ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝐴 𝐵 d 𝑥 )
11 5 10 eqtr2id ⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑦 ) d 𝑦 )