Metamath Proof Explorer

Theorem sge0sup

Description: The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0sup.x 
|- ( ph -> X e. V )
sge0sup.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion sge0sup 
|- ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )

Proof

Step Hyp Ref Expression
1 sge0sup.x 
 |-  ( ph -> X e. V )
2 sge0sup.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
3 eqidd 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo = +oo )
4 1 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> X e. V )
5 2 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
6 simpr 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
7 4 5 6 sge0pnfval 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = +oo )
8 vex 
 |-  x e. _V
9 8 a1i 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x e. _V )
10 2 adantr 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> F : X --> ( 0 [,] +oo ) )
11 elinel1 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. ~P X )
12 elpwi 
 |-  ( x e. ~P X -> x C_ X )
13 11 12 syl 
 |-  ( x e. ( ~P X i^i Fin ) -> x C_ X )
14 13 adantl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> x C_ X )
15 10 14 fssresd 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
16 9 15 sge0xrcl 
 |-  ( ( ph /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) e. RR* )
17 16 adantlr 
 |-  ( ( ( ph /\ +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) e. RR* )
18 17 ralrimiva 
 |-  ( ( ph /\ +oo e. ran F ) -> A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* )
19 eqid 
 |-  ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) = ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) )
20 19 rnmptss 
 |-  ( A. x e. ( ~P X i^i Fin ) ( sum^ ` ( F |` x ) ) e. RR* -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
21 18 20 syl 
 |-  ( ( ph /\ +oo e. ran F ) -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* )
22 2 ffnd 
 |-  ( ph -> F Fn X )
23 fvelrnb 
 |-  ( F Fn X -> ( +oo e. ran F <-> E. y e. X ( F ` y ) = +oo ) )
24 22 23 syl 
 |-  ( ph -> ( +oo e. ran F <-> E. y e. X ( F ` y ) = +oo ) )
25 24 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> ( +oo e. ran F <-> E. y e. X ( F ` y ) = +oo ) )
26 6 25 mpbid 
 |-  ( ( ph /\ +oo e. ran F ) -> E. y e. X ( F ` y ) = +oo )
27 snelpwi 
 |-  ( y e. X -> { y } e. ~P X )
28 snfi 
 |-  { y } e. Fin
29 28 a1i 
 |-  ( y e. X -> { y } e. Fin )
30 27 29 elind 
 |-  ( y e. X -> { y } e. ( ~P X i^i Fin ) )
31 30 3ad2ant2 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> { y } e. ( ~P X i^i Fin ) )
32 simp2 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> y e. X )
33 2 3ad2ant1 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> F : X --> ( 0 [,] +oo ) )
34 32 snssd 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> { y } C_ X )
35 33 34 fssresd 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( F |` { y } ) : { y } --> ( 0 [,] +oo ) )
36 32 35 sge0sn 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( sum^ ` ( F |` { y } ) ) = ( ( F |` { y } ) ` y ) )
37 vsnid 
 |-  y e. { y }
38 fvres 
 |-  ( y e. { y } -> ( ( F |` { y } ) ` y ) = ( F ` y ) )
39 37 38 ax-mp 
 |-  ( ( F |` { y } ) ` y ) = ( F ` y )
40 39 a1i 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( ( F |` { y } ) ` y ) = ( F ` y ) )
41 simp3 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> ( F ` y ) = +oo )
42 36 40 41 3eqtrrd 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo = ( sum^ ` ( F |` { y } ) ) )
43 reseq2 
 |-  ( x = { y } -> ( F |` x ) = ( F |` { y } ) )
44 43 fveq2d 
 |-  ( x = { y } -> ( sum^ ` ( F |` x ) ) = ( sum^ ` ( F |` { y } ) ) )
45 44 rspceeqv 
 |-  ( ( { y } e. ( ~P X i^i Fin ) /\ +oo = ( sum^ ` ( F |` { y } ) ) ) -> E. x e. ( ~P X i^i Fin ) +oo = ( sum^ ` ( F |` x ) ) )
46 31 42 45 syl2anc 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> E. x e. ( ~P X i^i Fin ) +oo = ( sum^ ` ( F |` x ) ) )
47 pnfex 
 |-  +oo e. _V
48 47 a1i 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo e. _V )
49 19 46 48 elrnmptd 
 |-  ( ( ph /\ y e. X /\ ( F ` y ) = +oo ) -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) )
50 49 3exp 
 |-  ( ph -> ( y e. X -> ( ( F ` y ) = +oo -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) ) )
51 50 rexlimdv 
 |-  ( ph -> ( E. y e. X ( F ` y ) = +oo -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) )
52 51 adantr 
 |-  ( ( ph /\ +oo e. ran F ) -> ( E. y e. X ( F ` y ) = +oo -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) )
53 26 52 mpd 
 |-  ( ( ph /\ +oo e. ran F ) -> +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) )
54 supxrpnf 
 |-  ( ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) C_ RR* /\ +oo e. ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = +oo )
55 21 53 54 syl2anc 
 |-  ( ( ph /\ +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = +oo )
56 3 7 55 3eqtr4d 
 |-  ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )
57 1 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> X e. V )
58 2 adantr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
59 simpr 
 |-  ( ( ph /\ -. +oo e. ran F ) -> -. +oo e. ran F )
60 58 59 fge0iccico 
 |-  ( ( ph /\ -. +oo e. ran F ) -> F : X --> ( 0 [,) +oo ) )
61 57 60 sge0reval 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
62 elinel2 
 |-  ( x e. ( ~P X i^i Fin ) -> x e. Fin )
63 62 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> x e. Fin )
64 15 adantlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,] +oo ) )
65 nelrnres 
 |-  ( -. +oo e. ran F -> -. +oo e. ran ( F |` x ) )
66 65 ad2antlr 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> -. +oo e. ran ( F |` x ) )
67 64 66 fge0iccico 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( F |` x ) : x --> ( 0 [,) +oo ) )
68 63 67 sge0fsum 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) = sum_ y e. x ( ( F |` x ) ` y ) )
69 simpr 
 |-  ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> y e. x )
70 fvres 
 |-  ( y e. x -> ( ( F |` x ) ` y ) = ( F ` y ) )
71 69 70 syl 
 |-  ( ( x e. ( ~P X i^i Fin ) /\ y e. x ) -> ( ( F |` x ) ` y ) = ( F ` y ) )
72 71 sumeq2dv 
 |-  ( x e. ( ~P X i^i Fin ) -> sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) )
73 72 adantl 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> sum_ y e. x ( ( F |` x ) ` y ) = sum_ y e. x ( F ` y ) )
74 68 73 eqtrd 
 |-  ( ( ( ph /\ -. +oo e. ran F ) /\ x e. ( ~P X i^i Fin ) ) -> ( sum^ ` ( F |` x ) ) = sum_ y e. x ( F ` y ) )
75 74 mpteq2dva 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) = ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
76 75 rneqd 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) = ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) )
77 76 supeq1d 
 |-  ( ( ph /\ -. +oo e. ran F ) -> sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
78 61 77 eqtr4d 
 |-  ( ( ph /\ -. +oo e. ran F ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )
79 56 78 pm2.61dan 
 |-  ( ph -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> ( sum^ ` ( F |` x ) ) ) , RR* , < ) )