Metamath Proof Explorer

Theorem sge0cl

Description: The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0cl.x 
|- ( ph -> X e. V )
sge0cl.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion sge0cl 
|- ( ph -> ( sum^ ` F ) e. ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 sge0cl.x 
 |-  ( ph -> X e. V )
2 sge0cl.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 fveq2 
 |-  ( F = (/) -> ( sum^ ` F ) = ( sum^ ` (/) ) )
4 sge00 
 |-  ( sum^ ` (/) ) = 0
5 4 a1i 
 |-  ( F = (/) -> ( sum^ ` (/) ) = 0 )
6 3 5 eqtrd 
 |-  ( F = (/) -> ( sum^ ` F ) = 0 )
7 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
8 7 a1i 
 |-  ( F = (/) -> 0 e. ( 0 [,] +oo ) )
9 6 8 eqeltrd 
 |-  ( F = (/) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
10 9 adantl 
 |-  ( ( ph /\ F = (/) ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
11 1 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> X e. V )
12 2 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
13 simpr 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
14 11 12 13 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = +oo )
15 pnfel0pnf 
 |-  +oo e. ( 0 [,] +oo )
16 15 a1i 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ( 0 [,] +oo ) )
17 14 16 eqeltrd 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
18 17 adantlr 
 |-  ( ( ( ph /\ -. F = (/) ) /\ +oo e. ran F ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
19 simpll 
 |-  ( ( ( ph /\ -. F = (/) ) /\ -. +oo e. ran F ) -> ph )
20 neqne 
 |-  ( -. F = (/) -> F =/= (/) )
21 20 ad2antlr 
 |-  ( ( ( ph /\ -. F = (/) ) /\ -. +oo e. ran F ) -> F =/= (/) )
22 simpr 
 |-  ( ( ( ph /\ -. F = (/) ) /\ -. +oo e. ran F ) -> -. +oo e. ran F )
23 0xr 
 |-  0 e. RR*
24 23 a1i 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> 0 e. RR* )
25 pnfxr 
 |-  +oo e. RR*
26 25 a1i 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> +oo e. RR* )
27 1 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> X e. V )
28 2 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
29 simpr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> -. +oo e. ran F )
30 28 29 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,) +oo ) )
31 27 30 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
32 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
33 32 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
34 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> F : X --> ( 0 [,] +oo ) )
35 elinel1 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. ~P X )
36 elpwi 
 |-  ( x e. ~P X -> x C_ X )
37 35 36 syl 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
38 37 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
39 38 adantr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> x C_ X )
40 simpr 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. x )
41 39 40 sseldd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> y e. X )
42 34 41 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,] +oo ) )
43 42 adantllr 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. ( 0 [,] +oo ) )
44 nne 
 |-  ( -. ( F ` y ) =/= +oo <-> ( F ` y ) = +oo )
45 44 biimpi 
 |-  ( -. ( F ` y ) =/= +oo -> ( F ` y ) = +oo )
46 45 eqcomd 
 |-  ( -. ( F ` y ) =/= +oo -> +oo = ( F ` y ) )
47 46 adantl 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ -. ( F ` y ) =/= +oo ) -> +oo = ( F ` y ) )
48 2 ffund 
 |-  ( ph -> Fun F )
49 48 3ad2ant1 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ y e. x ) -> Fun F )
50 41 3impa 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. X )
51 2 fdmd 
 |-  ( ph -> dom F = X )
52 51 eqcomd 
 |-  ( ph -> X = dom F )
53 52 3ad2ant1 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ y e. x ) -> X = dom F )
54 50 53 eleqtrd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. dom F )
55 fvelrn 
 |-  ( ( Fun F /\ y e. dom F ) -> ( F ` y ) e. ran F )
56 49 54 55 syl2anc 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) /\ y e. x ) -> ( F ` y ) e. ran F )
57 56 ad5ant134 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ -. ( F ` y ) =/= +oo ) -> ( F ` y ) e. ran F )
58 47 57 eqeltrd 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ -. ( F ` y ) =/= +oo ) -> +oo e. ran F )
59 29 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) /\ -. ( F ` y ) =/= +oo ) -> -. +oo e. ran F )
60 58 59 condan 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) =/= +oo )
61 ge0xrre 
 |-  ( ( ( F ` y ) e. ( 0 [,] +oo ) /\ ( F ` y ) =/= +oo ) -> ( F ` y ) e. RR )
62 43 60 61 syl2anc 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) /\ y e. x ) -> ( F ` y ) e. RR )
63 33 62 fsumrecl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( F ` y ) e. RR )
64 63 ralrimiva 
 |-  ( ( ph /\ -. +oo e. ran F ) -> A. x e. ( ~P X i^i Fin ) sum_ y e. x ( F ` y ) e. RR )
65 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) )
66 65 rnmptss 
 |-  ( A. x e. ( ~P X i^i Fin ) sum_ y e. x ( F ` y ) e. RR -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
67 64 66 syl 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
68 ressxr 
 |-  RR C_ RR*
69 68 a1i 
 |-  ( ( ph /\ -. +oo e. ran F ) -> RR C_ RR* )
70 67 69 sstrd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
71 supxrcl 
 |-  ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) e. RR* )
72 70 71 syl 
 |-  ( ( ph /\ -. +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) e. RR* )
73 31 72 eqeltrd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) e. RR* )
74 73 adantlr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> ( sum^ ` F ) e. RR* )
75 52 adantr 
 |-  ( ( ph /\ F =/= (/) ) -> X = dom F )
76 neneq 
 |-  ( F =/= (/) -> -. F = (/) )
77 76 adantl 
 |-  ( ( ph /\ F =/= (/) ) -> -. F = (/) )
78 frel 
 |-  ( F : X --> ( 0 [,] +oo ) -> Rel F )
79 2 78 syl 
 |-  ( ph -> Rel F )
80 79 adantr 
 |-  ( ( ph /\ F =/= (/) ) -> Rel F )
81 reldm0 
 |-  ( Rel F -> ( F = (/) <-> dom F = (/) ) )
82 80 81 syl 
 |-  ( ( ph /\ F =/= (/) ) -> ( F = (/) <-> dom F = (/) ) )
83 77 82 mtbid 
 |-  ( ( ph /\ F =/= (/) ) -> -. dom F = (/) )
84 83 neqned 
 |-  ( ( ph /\ F =/= (/) ) -> dom F =/= (/) )
85 75 84 eqnetrd 
 |-  ( ( ph /\ F =/= (/) ) -> X =/= (/) )
86 n0 
 |-  ( X =/= (/) <-> E. z z e. X )
87 85 86 sylib 
 |-  ( ( ph /\ F =/= (/) ) -> E. z z e. X )
88 87 adantr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> E. z z e. X )
89 23 a1i 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> 0 e. RR* )
90 2 ffvelcdmda 
 |-  ( ( ph /\ z e. X ) -> ( F ` z ) e. ( 0 [,] +oo ) )
91 90 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. ( 0 [,] +oo ) )
92 nne 
 |-  ( -. ( F ` z ) =/= +oo <-> ( F ` z ) = +oo )
93 92 biimpi 
 |-  ( -. ( F ` z ) =/= +oo -> ( F ` z ) = +oo )
94 93 eqcomd 
 |-  ( -. ( F ` z ) =/= +oo -> +oo = ( F ` z ) )
95 94 adantl 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) /\ -. ( F ` z ) =/= +oo ) -> +oo = ( F ` z ) )
96 2 adantr 
 |-  ( ( ph /\ z e. X ) -> F : X --> ( 0 [,] +oo ) )
97 96 ffund 
 |-  ( ( ph /\ z e. X ) -> Fun F )
98 simpr 
 |-  ( ( ph /\ z e. X ) -> z e. X )
99 52 adantr 
 |-  ( ( ph /\ z e. X ) -> X = dom F )
100 98 99 eleqtrd 
 |-  ( ( ph /\ z e. X ) -> z e. dom F )
101 fvelrn 
 |-  ( ( Fun F /\ z e. dom F ) -> ( F ` z ) e. ran F )
102 97 100 101 syl2anc 
 |-  ( ( ph /\ z e. X ) -> ( F ` z ) e. ran F )
103 102 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. ran F )
104 103 adantr 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) /\ -. ( F ` z ) =/= +oo ) -> ( F ` z ) e. ran F )
105 95 104 eqeltrd 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) /\ -. ( F ` z ) =/= +oo ) -> +oo e. ran F )
106 29 ad2antrr 
 |-  ( ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) /\ -. ( F ` z ) =/= +oo ) -> -. +oo e. ran F )
107 105 106 condan 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) =/= +oo )
108 ge0xrre 
 |-  ( ( ( F ` z ) e. ( 0 [,] +oo ) /\ ( F ` z ) =/= +oo ) -> ( F ` z ) e. RR )
109 91 107 108 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. RR )
110 109 rexrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. RR* )
111 73 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( sum^ ` F ) e. RR* )
112 23 a1i 
 |-  ( ( ph /\ z e. X ) -> 0 e. RR* )
113 25 a1i 
 |-  ( ( ph /\ z e. X ) -> +oo e. RR* )
114 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` z ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` z ) )
115 112 113 90 114 syl3anc 
 |-  ( ( ph /\ z e. X ) -> 0 <_ ( F ` z ) )
116 115 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> 0 <_ ( F ` z ) )
117 70 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* )
118 snelpwi 
 |-  ( z e. X -> { z } e. ~P X )
119 snfi 
 |-  { z } e. Fin
120 119 a1i 
 |-  ( z e. X -> { z } e. Fin )
121 118 120 elind 
 |-  ( z e. X -> { z } e. ( ~P X i^i Fin ) )
122 121 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> { z } e. ( ~P X i^i Fin ) )
123 simpr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> z e. X )
124 109 recnd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. CC )
125 fveq2 
 |-  ( y = z -> ( F ` y ) = ( F ` z ) )
126 125 sumsn 
 |-  ( ( z e. X /\ ( F ` z ) e. CC ) -> sum_ y e. { z } ( F ` y ) = ( F ` z ) )
127 123 124 126 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> sum_ y e. { z } ( F ` y ) = ( F ` z ) )
128 127 eqcomd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) = sum_ y e. { z } ( F ` y ) )
129 sumeq1 
 |-  ( x = { z } -> sum_ y e. x ( F ` y ) = sum_ y e. { z } ( F ` y ) )
130 129 rspceeqv 
 |-  ( ( { z } e. ( ~P X i^i Fin ) /\ ( F ` z ) = sum_ y e. { z } ( F ` y ) ) -> E. x e. ( ~P X i^i Fin ) ( F ` z ) = sum_ y e. x ( F ` y ) )
131 122 128 130 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> E. x e. ( ~P X i^i Fin ) ( F ` z ) = sum_ y e. x ( F ` y ) )
132 65 elrnmpt 
 |-  ( ( F ` z ) e. ( 0 [,] +oo ) -> ( ( F ` z ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) ( F ` z ) = sum_ y e. x ( F ` y ) ) )
133 91 132 syl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( ( F ` z ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) <-> E. x e. ( ~P X i^i Fin ) ( F ` z ) = sum_ y e. x ( F ` y ) ) )
134 131 133 mpbird 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
135 supxrub 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR* /\ ( F ` z ) e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) ) -> ( F ` z ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
136 117 134 135 syl2anc 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) <_ sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
137 31 eqcomd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = ( sum^ ` F ) )
138 137 adantr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = ( sum^ ` F ) )
139 136 138 breqtrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> ( F ` z ) <_ ( sum^ ` F ) )
140 89 110 111 116 139 xrletrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ z e. X ) -> 0 <_ ( sum^ ` F ) )
141 140 ex 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( z e. X -> 0 <_ ( sum^ ` F ) ) )
142 141 adantlr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> ( z e. X -> 0 <_ ( sum^ ` F ) ) )
143 142 exlimdv 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> ( E. z z e. X -> 0 <_ ( sum^ ` F ) ) )
144 88 143 mpd 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> 0 <_ ( sum^ ` F ) )
145 pnfge 
 |-  ( ( sum^ ` F ) e. RR* -> ( sum^ ` F ) <_ +oo )
146 73 145 syl 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) <_ +oo )
147 146 adantlr 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> ( sum^ ` F ) <_ +oo )
148 24 26 74 144 147 eliccxrd 
 |-  ( ( ( ph /\ F =/= (/) ) /\ -. +oo e. ran F ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
149 19 21 22 148 syl21anc 
 |-  ( ( ( ph /\ -. F = (/) ) /\ -. +oo e. ran F ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
150 18 149 pm2.61dan 
 |-  ( ( ph /\ -. F = (/) ) -> ( sum^ ` F ) e. ( 0 [,] +oo ) )
151 10 150 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) e. ( 0 [,] +oo ) )