Metamath Proof Explorer


Theorem cbvesum

Description: Change bound variable in an extended sum. (Contributed by Thierry Arnoux, 19-Jun-2017)

Ref Expression
Hypotheses cbvesum.1 ( 𝑗 = 𝑘𝐵 = 𝐶 )
cbvesum.2 𝑘 𝐴
cbvesum.3 𝑗 𝐴
cbvesum.4 𝑘 𝐵
cbvesum.5 𝑗 𝐶
Assertion cbvesum Σ* 𝑗𝐴 𝐵 = Σ* 𝑘𝐴 𝐶

Proof

Step Hyp Ref Expression
1 cbvesum.1 ( 𝑗 = 𝑘𝐵 = 𝐶 )
2 cbvesum.2 𝑘 𝐴
3 cbvesum.3 𝑗 𝐴
4 cbvesum.4 𝑘 𝐵
5 cbvesum.5 𝑗 𝐶
6 3 2 4 5 1 cbvmptf ( 𝑗𝐴𝐵 ) = ( 𝑘𝐴𝐶 )
7 6 oveq2i ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑗𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) )
8 7 unieqi ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑗𝐴𝐵 ) ) = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) )
9 df-esum Σ* 𝑗𝐴 𝐵 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑗𝐴𝐵 ) )
10 df-esum Σ* 𝑘𝐴 𝐶 = ( ( ℝ*𝑠s ( 0 [,] +∞ ) ) tsums ( 𝑘𝐴𝐶 ) )
11 8 9 10 3eqtr4i Σ* 𝑗𝐴 𝐵 = Σ* 𝑘𝐴 𝐶