Theorem sge0reval

Description: Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0reval.x	|- ( ph -> X e. V )
	sge0reval.f	|- ( ph -> F : X --> ( 0 [,) +oo ) )
Assertion	sge0reval	|- ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		sge0reval.x	|- ( ph -> X e. V )
2		sge0reval.f	|- ( ph -> F : X --> ( 0 [,) +oo ) )
3	2	fge0icoicc	|- ( ph -> F : X --> ( 0 [,] +oo ) )
4	1 3	sge0vald	|- ( ph -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) )
5	2	fge0npnf	|- ( ph -> -. +oo e. ran F )
6	5	iffalsed	|- ( ph -> if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
7	4 6	eqtrd	|- ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )