Theorem esumgsum

Description: A finite extended sum is the group sum over the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 24-Apr-2020)

	Ref	Expression
Hypotheses	esumgsum.1	|- F/ k ph
	esumgsum.2	|- F/_ k A
	esumgsum.3	|- ( ph -> A e. Fin )
	esumgsum.4	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
Assertion	esumgsum	|- ( ph -> sum* k e. A B = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )

Proof

Step	Hyp	Ref	Expression
1		esumgsum.1	|- F/ k ph
2		esumgsum.2	|- F/_ k A
3		esumgsum.3	|- ( ph -> A e. Fin )
4		esumgsum.4	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
5		xrge0base	|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
6		xrge00	|- 0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
7		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
8	7	a1i	|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
9		xrge0tps	|- ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
10	9	a1i	|- ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
11		nfcv	|- F/_ k ( 0 [,] +oo )
12		eqid	|- ( k e. A |-> B ) = ( k e. A |-> B )
13	1 2 11 4 12	fmptdF	|- ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
14	4	ex	|- ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
15	1 14	ralrimi	|- ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
16	2	fnmptf	|- ( A. k e. A B e. ( 0 [,] +oo ) -> ( k e. A |-> B ) Fn A )
17	15 16	syl	|- ( ph -> ( k e. A |-> B ) Fn A )
18		0xr	|- 0 e. RR*
19	18	a1i	|- ( ph -> 0 e. RR* )
20	17 3 19	fndmfifsupp	|- ( ph -> ( k e. A |-> B ) finSupp 0 )
21	5 6 8 10 3 13 20	tsmsid	|- ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) e. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) )
22	1 2 3 4 21	esumid	|- ( ph -> sum* k e. A B = ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. A |-> B ) ) )