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

Metamath Proof Explorer

Theorem cbvitgv

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

Ref Expression
Hypothesis cbvitg.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
Assertion cbvitgv ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑦

Proof

Step Hyp Ref Expression
1 cbvitg.1 ⊢ ( 𝑥 = 𝑦 → 𝐵 = 𝐶 )
2 1 fvoveq1d ⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
4 3 anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) ) )
5 4 ifbid ⊢ ( 𝑥 = 𝑦 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
6 2 5 csbeq12dv ⊢ ( 𝑥 = 𝑦 → ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) = ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
7 6 cbvmptv ⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) = ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) )
8 7 fveq2i ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) = ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) )
9 8 oveq2i ⊢ ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
10 9 a1i ⊢ ( ⊤ → ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) )
11 10 sumeq2sdv ⊢ ( ⊤ → Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) )
12 11 mptru ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
13 df-itg ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
14 df-itg ⊢ ∫ 𝐴 𝐶 d 𝑦 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑦 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) / 𝑣 ⦌ if ( ( 𝑦 ∈ 𝐴 ∧ 0 ≤ 𝑣 ) , 𝑣 , 0 ) ) ) )
15 12 13 14 3eqtr4i ⊢ ∫ 𝐴 𝐵 d 𝑥 = ∫ 𝐴 𝐶 d 𝑦