Theorem cbvesum

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

	Ref	Expression
Hypotheses	cbvesum.1	|- ( j = k -> B = C )
	cbvesum.2	|- F/_ k A
	cbvesum.3	|- F/_ j A
	cbvesum.4	|- F/_ k B
	cbvesum.5	|- F/_ j C
Assertion	cbvesum	|- sum* j e. A B = sum* k e. A C

Proof

Step	Hyp	Ref	Expression
1		cbvesum.1	|- ( j = k -> B = C )
2		cbvesum.2	|- F/_ k A
3		cbvesum.3	|- F/_ j A
4		cbvesum.4	|- F/_ k B
5		cbvesum.5	|- F/_ j C
6	3 2 4 5 1	cbvmptf	|- ( j e. A |-> B ) = ( k e. A |-> C )
7	6	oveq2i	|- ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
8	7	unieqi	|- U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
9		df-esum	|- sum* j e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( j e. A |-> B ) )
10		df-esum	|- sum* k e. A C = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> C ) )
11	8 9 10	3eqtr4i	|- sum* j e. A B = sum* k e. A C