# Metamath Proof Explorer

## Theorem sge0ssrempt

Description: If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ssrempt.xph ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
sge0ssrempt.a ${⊢}{\phi }\to {A}\in {V}$
sge0ssrempt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
sge0ssrempt.re ${⊢}{\phi }\to \mathrm{sum^}\left(\left({x}\in {A}⟼{B}\right)\right)\in ℝ$
sge0ssrempt.c ${⊢}{\phi }\to {C}\subseteq {A}$
Assertion sge0ssrempt ${⊢}{\phi }\to \mathrm{sum^}\left(\left({x}\in {C}⟼{B}\right)\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 sge0ssrempt.xph ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 sge0ssrempt.a ${⊢}{\phi }\to {A}\in {V}$
3 sge0ssrempt.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in \left[0,\mathrm{+\infty }\right]$
4 sge0ssrempt.re ${⊢}{\phi }\to \mathrm{sum^}\left(\left({x}\in {A}⟼{B}\right)\right)\in ℝ$
5 sge0ssrempt.c ${⊢}{\phi }\to {C}\subseteq {A}$
6 5 resmptd ${⊢}{\phi }\to {\left({x}\in {A}⟼{B}\right)↾}_{{C}}=\left({x}\in {C}⟼{B}\right)$
7 6 fveq2d ${⊢}{\phi }\to \mathrm{sum^}\left({\left({x}\in {A}⟼{B}\right)↾}_{{C}}\right)=\mathrm{sum^}\left(\left({x}\in {C}⟼{B}\right)\right)$
8 7 eqcomd ${⊢}{\phi }\to \mathrm{sum^}\left(\left({x}\in {C}⟼{B}\right)\right)=\mathrm{sum^}\left({\left({x}\in {A}⟼{B}\right)↾}_{{C}}\right)$
9 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
10 1 3 9 fmptdf ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶\left[0,\mathrm{+\infty }\right]$
11 2 10 4 sge0ssre ${⊢}{\phi }\to \mathrm{sum^}\left({\left({x}\in {A}⟼{B}\right)↾}_{{C}}\right)\in ℝ$
12 8 11 eqeltrd ${⊢}{\phi }\to \mathrm{sum^}\left(\left({x}\in {C}⟼{B}\right)\right)\in ℝ$