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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0reval.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
Assertion	sge0reval	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		sge0reval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0reval.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,) +∞ ) )
3	2	fge0icoicc	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4	1 3	sge0vald	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) )
5	2	fge0npnf	⊢ ( 𝜑 → ¬ +∞ ∈ ran 𝐹 )
6	5	iffalsed	⊢ ( 𝜑 → if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )
7	4 6	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) )