Theorem sge0fodjrn

Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0fodjrn.k	$$⊢Ⅎk\phi$$
	sge0fodjrn.n	$$⊢Ⅎn\phi$$
	sge0fodjrn.bd	$$⊢k=G\to B=D$$
	sge0fodjrn.c	$$⊢\phi \to C\in V$$
	sge0fodjrn.f	$$⊢\phi \to F:C\underset{onto}{⟶}A$$
	sge0fodjrn.dj	$$⊢\phi \to \underset{n\in C}{Disj}F\left(n\right)$$
	sge0fodjrn.fng	$$⊢\left(\phi \wedge n\in C\right)\to F\left(n\right)=G$$
	sge0fodjrn.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	sge0fodjrn.b0	$$⊢\left(\phi \wedge k=\varnothing \right)\to B=0$$
Assertion	sge0fodjrn	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)=\mathrm{sum^}\left(\left(n\in C⟼D\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0fodjrn.k	$$⊢Ⅎk\phi$$
2		sge0fodjrn.n	$$⊢Ⅎn\phi$$
3		sge0fodjrn.bd	$$⊢k=G\to B=D$$
4		sge0fodjrn.c	$$⊢\phi \to C\in V$$
5		sge0fodjrn.f	$$⊢\phi \to F:C\underset{onto}{⟶}A$$
6		sge0fodjrn.dj	$$⊢\phi \to \underset{n\in C}{Disj}F\left(n\right)$$
7		sge0fodjrn.fng	$$⊢\left(\phi \wedge n\in C\right)\to F\left(n\right)=G$$
8		sge0fodjrn.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
9		sge0fodjrn.b0	$$⊢\left(\phi \wedge k=\varnothing \right)\to B=0$$
10		eqid	$$⊢F^{-1}\left[\left\{\varnothing \right\}\right]=F^{-1}\left[\left\{\varnothing \right\}\right]$$
11	1 2 3 4 5 6 7 8 9 10	sge0fodjrnlem	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)=\mathrm{sum^}\left(\left(n\in C⟼D\right)\right)$$