Metamath Proof Explorer

Theorem sge0ssre

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 sge0less.x 
|- ( ph -> X e. V )
sge0less.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
sge0ssre.re 
|- ( ph -> ( sum^ ` F ) e. RR )
Assertion sge0ssre 
|- ( ph -> ( sum^ ` ( F |` Y ) ) e. RR )

Proof

Step Hyp Ref Expression
1 sge0less.x 
 |-  ( ph -> X e. V )
2 sge0less.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 sge0ssre.re 
 |-  ( ph -> ( sum^ ` F ) e. RR )
4 inex1g 
 |-  ( X e. V -> ( X i^i Y ) e. _V )
5 1 4 syl 
 |-  ( ph -> ( X i^i Y ) e. _V )
6 fresin 
 |-  ( F : X --> ( 0 [,] +oo ) -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,] +oo ) )
7 2 6 syl 
 |-  ( ph -> ( F |` Y ) : ( X i^i Y ) --> ( 0 [,] +oo ) )
8 5 7 sge0xrcl 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) e. RR* )
9 mnfxr 
 |-  -oo e. RR*
10 9 a1i 
 |-  ( ph -> -oo e. RR* )
11 0xr 
 |-  0 e. RR*
12 11 a1i 
 |-  ( ph -> 0 e. RR* )
13 mnflt0 
 |-  -oo < 0
14 13 a1i 
 |-  ( ph -> -oo < 0 )
15 5 7 sge0ge0 
 |-  ( ph -> 0 <_ ( sum^ ` ( F |` Y ) ) )
16 10 12 8 14 15 xrltletrd 
 |-  ( ph -> -oo < ( sum^ ` ( F |` Y ) ) )
17 1 2 sge0less 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) )
18 xrre 
 |-  ( ( ( ( sum^ ` ( F |` Y ) ) e. RR* /\ ( sum^ ` F ) e. RR ) /\ ( -oo < ( sum^ ` ( F |` Y ) ) /\ ( sum^ ` ( F |` Y ) ) <_ ( sum^ ` F ) ) ) -> ( sum^ ` ( F |` Y ) ) e. RR )
19 8 3 16 17 18 syl22anc 
 |-  ( ph -> ( sum^ ` ( F |` Y ) ) e. RR )