Metamath Proof Explorer


Theorem sge0sn

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0sn.1
|- ( ph -> A e. V )
sge0sn.2
|- ( ph -> F : { A } --> ( 0 [,] +oo ) )
Assertion sge0sn
|- ( ph -> ( sum^ ` F ) = ( F ` A ) )

Proof

Step Hyp Ref Expression
1 sge0sn.1
 |-  ( ph -> A e. V )
2 sge0sn.2
 |-  ( ph -> F : { A } --> ( 0 [,] +oo ) )
3 snex
 |-  { A } e. _V
4 3 a1i
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> { A } e. _V )
5 2 adantr
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
6 id
 |-  ( ( F ` A ) = +oo -> ( F ` A ) = +oo )
7 6 eqcomd
 |-  ( ( F ` A ) = +oo -> +oo = ( F ` A ) )
8 7 adantl
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> +oo = ( F ` A ) )
9 2 ffund
 |-  ( ph -> Fun F )
10 9 adantr
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> Fun F )
11 snidg
 |-  ( A e. V -> A e. { A } )
12 1 11 syl
 |-  ( ph -> A e. { A } )
13 2 fdmd
 |-  ( ph -> dom F = { A } )
14 13 eqcomd
 |-  ( ph -> { A } = dom F )
15 12 14 eleqtrd
 |-  ( ph -> A e. dom F )
16 15 adantr
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> A e. dom F )
17 fvelrn
 |-  ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
18 10 16 17 syl2anc
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) e. ran F )
19 8 18 eqeltrd
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> +oo e. ran F )
20 4 5 19 sge0pnfval
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> ( sum^ ` F ) = +oo )
21 simpr
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) = +oo )
22 20 21 eqtr4d
 |-  ( ( ph /\ ( F ` A ) = +oo ) -> ( sum^ ` F ) = ( F ` A ) )
23 3 a1i
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> { A } e. _V )
24 2 adantr
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
25 elsni
 |-  ( +oo e. { ( F ` A ) } -> +oo = ( F ` A ) )
26 25 eqcomd
 |-  ( +oo e. { ( F ` A ) } -> ( F ` A ) = +oo )
27 26 con3i
 |-  ( -. ( F ` A ) = +oo -> -. +oo e. { ( F ` A ) } )
28 27 adantl
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. { ( F ` A ) } )
29 1 2 rnsnf
 |-  ( ph -> ran F = { ( F ` A ) } )
30 29 eqcomd
 |-  ( ph -> { ( F ` A ) } = ran F )
31 30 adantr
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> { ( F ` A ) } = ran F )
32 28 31 neleqtrd
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. ran F )
33 24 32 fge0iccico
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,) +oo ) )
34 23 33 sge0reval
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( sum^ ` F ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
35 sum0
 |-  sum_ y e. (/) ( F ` y ) = 0
36 35 eqcomi
 |-  0 = sum_ y e. (/) ( F ` y )
37 36 a1i
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> 0 = sum_ y e. (/) ( F ` y ) )
38 nfcvd
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> F/_ y ( F ` A ) )
39 nfv
 |-  F/ y ( ph /\ -. ( F ` A ) = +oo )
40 fveq2
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
41 40 adantl
 |-  ( ( ( ph /\ -. ( F ` A ) = +oo ) /\ y = A ) -> ( F ` y ) = ( F ` A ) )
42 1 adantr
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. V )
43 rge0ssre
 |-  ( 0 [,) +oo ) C_ RR
44 ax-resscn
 |-  RR C_ CC
45 43 44 sstri
 |-  ( 0 [,) +oo ) C_ CC
46 42 11 syl
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. { A } )
47 33 46 ffvelrnd
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. ( 0 [,) +oo ) )
48 45 47 sseldi
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. CC )
49 38 39 41 42 48 sumsnd
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> sum_ y e. { A } ( F ` y ) = ( F ` A ) )
50 49 eqcomd
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sum_ y e. { A } ( F ` y ) )
51 37 50 preq12d
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> { 0 , ( F ` A ) } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } )
52 51 supeq1d
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) )
53 xrltso
 |-  < Or RR*
54 53 a1i
 |-  ( ph -> < Or RR* )
55 0xr
 |-  0 e. RR*
56 55 a1i
 |-  ( ph -> 0 e. RR* )
57 iccssxr
 |-  ( 0 [,] +oo ) C_ RR*
58 2 12 ffvelrnd
 |-  ( ph -> ( F ` A ) e. ( 0 [,] +oo ) )
59 57 58 sseldi
 |-  ( ph -> ( F ` A ) e. RR* )
60 suppr
 |-  ( ( < Or RR* /\ 0 e. RR* /\ ( F ` A ) e. RR* ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) )
61 54 56 59 60 syl3anc
 |-  ( ph -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) )
62 pnfxr
 |-  +oo e. RR*
63 62 a1i
 |-  ( ph -> +oo e. RR* )
64 56 63 58 3jca
 |-  ( ph -> ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) )
65 iccgelb
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` A ) )
66 64 65 syl
 |-  ( ph -> 0 <_ ( F ` A ) )
67 56 59 xrlenltd
 |-  ( ph -> ( 0 <_ ( F ` A ) <-> -. ( F ` A ) < 0 ) )
68 66 67 mpbid
 |-  ( ph -> -. ( F ` A ) < 0 )
69 68 iffalsed
 |-  ( ph -> if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) = ( F ` A ) )
70 61 69 eqtr2d
 |-  ( ph -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
71 70 adantr
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
72 pwsn
 |-  ~P { A } = { (/) , { A } }
73 72 ineq1i
 |-  ( ~P { A } i^i Fin ) = ( { (/) , { A } } i^i Fin )
74 0fin
 |-  (/) e. Fin
75 snfi
 |-  { A } e. Fin
76 prssi
 |-  ( ( (/) e. Fin /\ { A } e. Fin ) -> { (/) , { A } } C_ Fin )
77 74 75 76 mp2an
 |-  { (/) , { A } } C_ Fin
78 df-ss
 |-  ( { (/) , { A } } C_ Fin <-> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } )
79 78 biimpi
 |-  ( { (/) , { A } } C_ Fin -> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } )
80 77 79 ax-mp
 |-  ( { (/) , { A } } i^i Fin ) = { (/) , { A } }
81 73 80 eqtri
 |-  ( ~P { A } i^i Fin ) = { (/) , { A } }
82 mpteq1
 |-  ( ( ~P { A } i^i Fin ) = { (/) , { A } } -> ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) )
83 81 82 ax-mp
 |-  ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) )
84 0ex
 |-  (/) e. _V
85 84 a1i
 |-  ( T. -> (/) e. _V )
86 3 a1i
 |-  ( T. -> { A } e. _V )
87 sumex
 |-  sum_ y e. (/) ( F ` y ) e. _V
88 87 a1i
 |-  ( T. -> sum_ y e. (/) ( F ` y ) e. _V )
89 sumex
 |-  sum_ y e. { A } ( F ` y ) e. _V
90 89 a1i
 |-  ( T. -> sum_ y e. { A } ( F ` y ) e. _V )
91 sumeq1
 |-  ( x = (/) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
92 91 adantl
 |-  ( ( T. /\ x = (/) ) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
93 sumeq1
 |-  ( x = { A } -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
94 93 adantl
 |-  ( ( T. /\ x = { A } ) -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
95 85 86 88 90 92 94 fmptpr
 |-  ( T. -> { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) )
96 95 mptru
 |-  { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) )
97 96 eqcomi
 |-  ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) = { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. }
98 83 97 eqtri
 |-  ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. }
99 98 rneqi
 |-  ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. }
100 rnpropg
 |-  ( ( (/) e. _V /\ { A } e. _V ) -> ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } )
101 84 3 100 mp2an
 |-  ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) }
102 99 101 eqtri
 |-  ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) }
103 102 supeq1i
 |-  sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < )
104 103 a1i
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) )
105 52 71 104 3eqtr4d
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
106 34 105 eqtr4d
 |-  ( ( ph /\ -. ( F ` A ) = +oo ) -> ( sum^ ` F ) = ( F ` A ) )
107 22 106 pm2.61dan
 |-  ( ph -> ( sum^ ` F ) = ( F ` A ) )