Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sge0vald.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
| sge0vald.f | ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) | ||
| Assertion | sge0vald | ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sge0vald.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
| 2 | sge0vald.f | ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) | |
| 3 | sge0val | ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) ) | |
| 4 | 1 2 3 | syl2anc | ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) ) |