Theorem esumrnmpt

Description: Rewrite an extended sum into a sum on the range of a mapping function. (Contributed by Thierry Arnoux, 27-May-2020)

	Ref	Expression
Hypotheses	esumrnmpt.0	|- F/_ k A
	esumrnmpt.1	|- ( y = B -> C = D )
	esumrnmpt.2	|- ( ph -> A e. V )
	esumrnmpt.3	|- ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )
	esumrnmpt.4	|- ( ( ph /\ k e. A ) -> B e. ( W \ { (/) } ) )
	esumrnmpt.5	|- ( ph -> Disj_ k e. A B )
Assertion	esumrnmpt	|- ( ph -> sum* y e. ran ( k e. A |-> B ) C = sum* k e. A D )

Proof

Step	Hyp	Ref	Expression
1		esumrnmpt.0	|- F/_ k A
2		esumrnmpt.1	|- ( y = B -> C = D )
3		esumrnmpt.2	|- ( ph -> A e. V )
4		esumrnmpt.3	|- ( ( ph /\ k e. A ) -> D e. ( 0 [,] +oo ) )
5		esumrnmpt.4	|- ( ( ph /\ k e. A ) -> B e. ( W \ { (/) } ) )
6		esumrnmpt.5	|- ( ph -> Disj_ k e. A B )
7		eqid	|- ( k e. A |-> B ) = ( k e. A |-> B )
8	7	rnmpt	|- ran ( k e. A |-> B ) = { z | E. k e. A z = B }
9		esumeq1	|- ( ran ( k e. A |-> B ) = { z | E. k e. A z = B } -> sum* y e. ran ( k e. A |-> B ) C = sum* y e. { z | E. k e. A z = B } C )
10	8 9	ax-mp	|- sum* y e. ran ( k e. A |-> B ) C = sum* y e. { z | E. k e. A z = B } C
11		nfcv	|- F/_ k C
12		nfv	|- F/ k ph
13	12 1 5 6	disjdsct	|- ( ph -> Fun `' ( k e. A |-> B ) )
14	11 12 1 2 3 13 4 5	esumc	|- ( ph -> sum* k e. A D = sum* y e. { z | E. k e. A z = B } C )
15	10 14	eqtr4id	|- ( ph -> sum* y e. ran ( k e. A |-> B ) C = sum* k e. A D )