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