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 𝑦