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	|- F/ k ph
	sge0fodjrn.n	|- F/ n ph
	sge0fodjrn.bd	|- ( k = G -> B = D )
	sge0fodjrn.c	|- ( ph -> C e. V )
	sge0fodjrn.f	|- ( ph -> F : C -onto-> A )
	sge0fodjrn.dj	|- ( ph -> Disj_ n e. C ( F ` n ) )
	sge0fodjrn.fng	|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
	sge0fodjrn.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
	sge0fodjrn.b0	|- ( ( ph /\ k = (/) ) -> B = 0 )
Assertion	sge0fodjrn	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )

Proof

Step	Hyp	Ref	Expression
1		sge0fodjrn.k	|- F/ k ph
2		sge0fodjrn.n	|- F/ n ph
3		sge0fodjrn.bd	|- ( k = G -> B = D )
4		sge0fodjrn.c	|- ( ph -> C e. V )
5		sge0fodjrn.f	|- ( ph -> F : C -onto-> A )
6		sge0fodjrn.dj	|- ( ph -> Disj_ n e. C ( F ` n ) )
7		sge0fodjrn.fng	|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
8		sge0fodjrn.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
9		sge0fodjrn.b0	|- ( ( ph /\ k = (/) ) -> B = 0 )
10		eqid	|- ( `' F " { (/) } ) = ( `' F " { (/) } )
11	1 2 3 4 5 6 7 8 9 10	sge0fodjrnlem	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = ( sum^ ` ( n e. C |-> D ) ) )