Metamath Proof Explorer


Theorem sge0fsum

Description: The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0fsum.x
|- ( ph -> X e. Fin )
sge0fsum.f
|- ( ph -> F : X --> ( 0 [,) +oo ) )
Assertion sge0fsum
|- ( ph -> ( sum^ ` F ) = sum_ x e. X ( F ` x ) )

Proof

Step Hyp Ref Expression
1 sge0fsum.x
 |-  ( ph -> X e. Fin )
2 sge0fsum.f
 |-  ( ph -> F : X --> ( 0 [,) +oo ) )
3 2 fge0icoicc
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
4 1 3 sge0xrcl
 |-  ( ph -> ( sum^ ` F ) e. RR* )
5 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
6 2 ffvelrnda
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( 0 [,) +oo ) )
7 5 6 sseldi
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR )
8 1 7 fsumrecl
 |-  ( ph -> sum_ x e. X ( F ` x ) e. RR )
9 8 rexrd
 |-  ( ph -> sum_ x e. X ( F ` x ) e. RR* )
10 1 2 sge0reval
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) )
11 simpr
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) )
12 vex
 |-  w e. _V
13 12 a1i
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w e. _V )
14 eqid
 |-  ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) = ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) )
15 14 elrnmpt
 |-  ( w e. _V -> ( w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) <-> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) ) )
16 13 15 syl
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> ( w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) <-> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) ) )
17 11 16 mpbid
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) )
18 simp3
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> w = sum_ x e. y ( F ` x ) )
19 1 adantr
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> X e. Fin )
20 2 fge0npnf
 |-  ( ph -> -. +oo e. ran F )
21 3 20 fge0iccre
 |-  ( ph -> F : X --> RR )
22 21 adantr
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> F : X --> RR )
23 22 adantr
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> F : X --> RR )
24 simpr
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> x e. X )
25 23 24 ffvelrnd
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> ( F ` x ) e. RR )
26 0xr
 |-  0 e. RR*
27 26 a1i
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> 0 e. RR* )
28 pnfxr
 |-  +oo e. RR*
29 28 a1i
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> +oo e. RR* )
30 3 adantr
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
31 30 ffvelrnda
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> ( F ` x ) e. ( 0 [,] +oo ) )
32 iccgelb
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` x ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` x ) )
33 27 29 31 32 syl3anc
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. X ) -> 0 <_ ( F ` x ) )
34 elinel1
 |-  ( y e. ( ~P X i^i Fin ) -> y e. ~P X )
35 elpwi
 |-  ( y e. ~P X -> y C_ X )
36 34 35 syl
 |-  ( y e. ( ~P X i^i Fin ) -> y C_ X )
37 36 adantl
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> y C_ X )
38 19 25 33 37 fsumless
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) <_ sum_ x e. X ( F ` x ) )
39 38 3adant3
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> sum_ x e. y ( F ` x ) <_ sum_ x e. X ( F ` x ) )
40 18 39 eqbrtrd
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) /\ w = sum_ x e. y ( F ` x ) ) -> w <_ sum_ x e. X ( F ` x ) )
41 40 3exp
 |-  ( ph -> ( y e. ( ~P X i^i Fin ) -> ( w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) ) )
42 41 rexlimdv
 |-  ( ph -> ( E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) )
43 42 adantr
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> ( E. y e. ( ~P X i^i Fin ) w = sum_ x e. y ( F ` x ) -> w <_ sum_ x e. X ( F ` x ) ) )
44 17 43 mpd
 |-  ( ( ph /\ w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) ) -> w <_ sum_ x e. X ( F ` x ) )
45 44 ralrimiva
 |-  ( ph -> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) )
46 elinel2
 |-  ( y e. ( ~P X i^i Fin ) -> y e. Fin )
47 46 adantl
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> y e. Fin )
48 22 adantr
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> F : X --> RR )
49 37 sselda
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> x e. X )
50 48 49 ffvelrnd
 |-  ( ( ( ph /\ y e. ( ~P X i^i Fin ) ) /\ x e. y ) -> ( F ` x ) e. RR )
51 47 50 fsumrecl
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) e. RR )
52 51 rexrd
 |-  ( ( ph /\ y e. ( ~P X i^i Fin ) ) -> sum_ x e. y ( F ` x ) e. RR* )
53 52 ralrimiva
 |-  ( ph -> A. y e. ( ~P X i^i Fin ) sum_ x e. y ( F ` x ) e. RR* )
54 14 rnmptss
 |-  ( A. y e. ( ~P X i^i Fin ) sum_ x e. y ( F ` x ) e. RR* -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* )
55 53 54 syl
 |-  ( ph -> ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* )
56 supxrleub
 |-  ( ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) C_ RR* /\ sum_ x e. X ( F ` x ) e. RR* ) -> ( sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) <-> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) ) )
57 55 9 56 syl2anc
 |-  ( ph -> ( sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) <-> A. w e. ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) w <_ sum_ x e. X ( F ` x ) ) )
58 45 57 mpbird
 |-  ( ph -> sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ x e. y ( F ` x ) ) , RR* , < ) <_ sum_ x e. X ( F ` x ) )
59 10 58 eqbrtrd
 |-  ( ph -> ( sum^ ` F ) <_ sum_ x e. X ( F ` x ) )
60 ssid
 |-  X C_ X
61 60 a1i
 |-  ( ph -> X C_ X )
62 1 2 61 1 fsumlesge0
 |-  ( ph -> sum_ x e. X ( F ` x ) <_ ( sum^ ` F ) )
63 4 9 59 62 xrletrid
 |-  ( ph -> ( sum^ ` F ) = sum_ x e. X ( F ` x ) )