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 sselid 
 |-  ( ( 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 ) )