Theorem sge0sn 38221

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

Hypotheses

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

Assertion

Ref	Expression
sge0sn	|- ( ph -> (Σ^ ` F ) = ( F ` A ) )

Proof of Theorem sge0sn

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		snex 4641	. . . . 5 |- { A } e. _V
2	1	a1i 11	. . . 4 |- ( ( ph /\ ( F ` A ) = +oo ) -> { A } e. _V )
3		sge0sn.2	. . . . 5 |- ( ph -> F : { A } --> ( 0 [,] +oo ) )
4	3	adantr 467	. . . 4 |- ( ( ph /\ ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
5		id 22	. . . . . . 7 |- ( ( F ` A ) = +oo -> ( F ` A ) = +oo )
6	5	eqcomd 2457	. . . . . 6 |- ( ( F ` A ) = +oo -> +oo = ( F ` A ) )
7	6	adantl 468	. . . . 5 |- ( ( ph /\ ( F ` A ) = +oo ) -> +oo = ( F ` A ) )
8		ffun 5731	. . . . . . . 8 |- ( F : { A } --> ( 0 [,] +oo ) -> Fun F )
9	3, 8	syl 17	. . . . . . 7 |- ( ph -> Fun F )
10	9	adantr 467	. . . . . 6 |- ( ( ph /\ ( F ` A ) = +oo ) -> Fun F )
11		sge0sn.1	. . . . . . . . 9 |- ( ph -> A e. V )
12		snidg 3994	. . . . . . . . 9 |- ( A e. V -> A e. { A } )
13	11, 12	syl 17	. . . . . . . 8 |- ( ph -> A e. { A } )
14		fdm 5733	. . . . . . . . . 10 |- ( F : { A } --> ( 0 [,] +oo ) -> dom F = { A } )
15	3, 14	syl 17	. . . . . . . . 9 |- ( ph -> dom F = { A } )
16	15	eqcomd 2457	. . . . . . . 8 |- ( ph -> { A } = dom F )
17	13, 16	eleqtrd 2531	. . . . . . 7 |- ( ph -> A e. dom F )
18	17	adantr 467	. . . . . 6 |- ( ( ph /\ ( F ` A ) = +oo ) -> A e. dom F )
19		fvelrn 6015	. . . . . 6 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
20	10, 18, 19	syl2anc 667	. . . . 5 |- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) e. ran F )
21	7, 20	eqeltrd 2529	. . . 4 |- ( ( ph /\ ( F ` A ) = +oo ) -> +oo e. ran F )
22	2, 4, 21	sge0pnfval 38215	. . 3 |- ( ( ph /\ ( F ` A ) = +oo ) -> (Σ^ ` F ) = +oo )
23		simpr 463	. . 3 |- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) = +oo )
24	22, 23	eqtr4d 2488	. 2 |- ( ( ph /\ ( F ` A ) = +oo ) -> (Σ^ ` F ) = ( F ` A ) )
25	1	a1i 11	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { A } e. _V )
26	3	adantr 467	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
27		elsni 3993	. . . . . . . . 9 |- ( +oo e. { ( F ` A ) } -> +oo = ( F ` A ) )
28	27	eqcomd 2457	. . . . . . . 8 |- ( +oo e. { ( F ` A ) } -> ( F ` A ) = +oo )
29	28	con3i 141	. . . . . . 7 |- ( -. ( F ` A ) = +oo -> -. +oo e. { ( F ` A ) } )
30	29	adantl 468	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. { ( F ` A ) } )
31	11, 3	rnsnf 37458	. . . . . . . 8 |- ( ph -> ran F = { ( F ` A ) } )
32	31	eqcomd 2457	. . . . . . 7 |- ( ph -> { ( F ` A ) } = ran F )
33	32	adantr 467	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { ( F ` A ) } = ran F )
34	30, 33	neleqtrd 2550	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. ran F )
35	26, 34	fge0iccico 38212	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,) +oo ) )
36	25, 35	sge0reval 38214	. . 3 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
37		sum0 13787	. . . . . . . 8 |- sum_ y e. (/) ( F ` y ) = 0
38	37	eqcomi 2460	. . . . . . 7 |- 0 = sum_ y e. (/) ( F ` y )
39	38	a1i 11	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> 0 = sum_ y e. (/) ( F ` y ) )
40		nfcvd 2593	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F/_ y ( F ` A ) )
41		nfv 1761	. . . . . . . 8 |- F/ y ( ph /\ -. ( F ` A ) = +oo )
42		fveq2 5865	. . . . . . . . 9 |- ( y = A -> ( F ` y ) = ( F ` A ) )
43	42	adantl 468	. . . . . . . 8 |- ( ( ( ph /\ -. ( F ` A ) = +oo ) /\ y = A ) -> ( F ` y ) = ( F ` A ) )
44	11	adantr 467	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. V )
45		rge0ssre 11740	. . . . . . . . . 10 |- ( 0 [,) +oo ) C_ RR
46		ax-resscn 9596	. . . . . . . . . 10 |- RR C_ CC
47	45, 46	sstri 3441	. . . . . . . . 9 |- ( 0 [,) +oo ) C_ CC
48	44, 12	syl 17	. . . . . . . . . 10 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. { A } )
49	35, 48	ffvelrnd 6023	. . . . . . . . 9 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. ( 0 [,) +oo ) )
50	47, 49	sseldi 3430	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. CC )
51	40, 41, 43, 44, 50	sumsnd 37347	. . . . . . 7 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> sum_ y e. { A } ( F ` y ) = ( F ` A ) )
52	51	eqcomd 2457	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sum_ y e. { A } ( F ` y ) )
53	39, 52	preq12d 4059	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { 0 , ( F ` A ) } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } )
54	53	supeq1d 7960	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = sup ( { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } , RR* , < ) )
55		xrltso 11440	. . . . . . . 8 |- < Or RR*
56	55	a1i 11	. . . . . . 7 |- ( ph -> < Or RR* )
57		0xr 9687	. . . . . . . 8 |- 0 e. RR*
58	57	a1i 11	. . . . . . 7 |- ( ph -> 0 e. RR* )
59		iccssxr 11717	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
60	3, 13	ffvelrnd 6023	. . . . . . . 8 |- ( ph -> ( F ` A ) e. ( 0 [,] +oo ) )
61	59, 60	sseldi 3430	. . . . . . 7 |- ( ph -> ( F ` A ) e. RR* )
62		suppr 7987	. . . . . . 7 |- ( ( < Or RR* /\ 0 e. RR* /\ ( F ` A ) e. RR* ) -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) )
63	56, 58, 61, 62	syl3anc 1268	. . . . . 6 |- ( ph -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) )
64		pnfxr 11412	. . . . . . . . . . 11 |- +oo e. RR*
65	64	a1i 11	. . . . . . . . . 10 |- ( ph -> +oo e. RR* )
66	58, 65, 60	3jca 1188	. . . . . . . . 9 |- ( ph -> ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) )
67		iccgelb 11691	. . . . . . . . 9 |- ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` A ) )
68	66, 67	syl 17	. . . . . . . 8 |- ( ph -> 0 <_ ( F ` A ) )
69	58, 61	xrlenltd 9700	. . . . . . . 8 |- ( ph -> ( 0 <_ ( F ` A ) <-> -. ( F ` A ) < 0 ) )
70	68, 69	mpbid 214	. . . . . . 7 |- ( ph -> -. ( F ` A ) < 0 )
71	70	iffalsed 3892	. . . . . 6 |- ( ph -> if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) = ( F ` A ) )
72	63, 71	eqtr2d 2486	. . . . 5 |- ( ph -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
73	72	adantr 467	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
74		pwsn 4192	. . . . . . . . . . . 12 |- ~P { A } = { (/) , { A } }
75	74	ineq1i 3630	. . . . . . . . . . 11 |- ( ~P { A } i^i Fin ) = ( { (/) , { A } } i^i Fin )
76		0fin 7799	. . . . . . . . . . . . 13 |- (/) e. Fin
77		snfi 7650	. . . . . . . . . . . . 13 |- { A } e. Fin
78		prssi 4128	. . . . . . . . . . . . 13 |- ( ( (/) e. Fin /\ { A } e. Fin ) -> { (/) , { A } } C_ Fin )
79	76, 77, 78	mp2an 678	. . . . . . . . . . . 12 |- { (/) , { A } } C_ Fin
80		df-ss 3418	. . . . . . . . . . . . 13 |- ( { (/) , { A } } C_ Fin <-> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } )
81	80	biimpi 198	. . . . . . . . . . . 12 |- ( { (/) , { A } } C_ Fin -> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } )
82	79, 81	ax-mp 5	. . . . . . . . . . 11 |- ( { (/) , { A } } i^i Fin ) = { (/) , { A } }
83	75, 82	eqtri 2473	. . . . . . . . . 10 |- ( ~P { A } i^i Fin ) = { (/) , { A } }
84		mpteq1 4483	. . . . . . . . . 10 |- ( ( ~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 ) ) )
85	83, 84	ax-mp 5	. . . . . . . . 9 |- ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) )
86		0ex 4535	. . . . . . . . . . . . 13 |- (/) e. _V
87	86	a1i 11	. . . . . . . . . . . 12 |- ( T. -> (/) e. _V )
88	1	a1i 11	. . . . . . . . . . . 12 |- ( T. -> { A } e. _V )
89		sumex 13754	. . . . . . . . . . . . 13 |- sum_ y e. (/) ( F ` y ) e. _V
90	89	a1i 11	. . . . . . . . . . . 12 |- ( T. -> sum_ y e. (/) ( F ` y ) e. _V )
91		sumex 13754	. . . . . . . . . . . . 13 |- sum_ y e. { A } ( F ` y ) e. _V
92	91	a1i 11	. . . . . . . . . . . 12 |- ( T. -> sum_ y e. { A } ( F ` y ) e. _V )
93		sumeq1 13755	. . . . . . . . . . . . 13 |- ( x = (/) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
94	93	adantl 468	. . . . . . . . . . . 12 |- ( ( T. /\ x = (/) ) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
95		sumeq1 13755	. . . . . . . . . . . . 13 |- ( x = { A } -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
96	95	adantl 468	. . . . . . . . . . . 12 |- ( ( T. /\ x = { A } ) -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
97	87, 88, 90, 92, 94, 96	fmptpr 6089	. . . . . . . . . . 11 |- ( T. -> { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) )
98	97	trud 1453	. . . . . . . . . 10 |- { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) )
99	98	eqcomi 2460	. . . . . . . . 9 |- ( x e. { (/) , { A } } |-> sum_ y e. x ( F ` y ) ) = { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. }
100	85, 99	eqtri 2473	. . . . . . . 8 |- ( 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 ) >. }
101	100	rneqi 5061	. . . . . . 7 |- 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 ) >. }
102		rnpropg 5316	. . . . . . . 8 |- ( ( (/) 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 ) } )
103	86, 1, 102	mp2an 678	. . . . . . 7 |- ran { <. (/) , sum_ y e. (/) ( F ` y ) >. , <. { A } , sum_ y e. { A } ( F ` y ) >. } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) }
104	101, 103	eqtri 2473	. . . . . 6 |- 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 ) }
105	104	supeq1i 7961	. . . . 5 |- 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* , < )
106	105	a1i 11	. . . 4 |- ( ( 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* , < ) )
107	54, 73, 106	3eqtr4d 2495	. . 3 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
108	36, 107	eqtr4d 2488	. 2 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> (Σ^ ` F ) = ( F ` A ) )
109	24, 108	pm2.61dan 800	1 |- ( ph -> (Σ^ ` F ) = ( F ` A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   /\ w3a 985   = wceq 1444   T. wtru 1445   e. wcel 1887   _Vcvv 3045   i^i cin 3403   C_ wss 3404   (/)c0 3731   ifcif 3881   ~Pcpw 3951   {csn 3968   {cpr 3970   <.cop 3974   class class class wbr 4402   |-> cmpt 4461   Or wor 4754   dom cdm 4834   ran crn 4835   Fun wfun 5576   -->wf 5578   ` cfv 5582  (class class class)co 6290   Fincfn 7569   supcsup 7954   CCcc 9537   RRcr 9538   0cc0 9539   +oocpnf 9672   RR*cxr 9674   < clt 9675   <_ cle 9676   [,)cico 11637   [,]cicc 11638   sum_csu 13752  Σ^{^}csumge0 38204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-sup 7956  df-oi 8025  df-card 8373  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-clim 13552  df-sum 13753  df-sumge0 38205

This theorem is referenced by:  sge0snmpt  38225  sge0sup  38233  sge0snmptf  38279  caratheodorylem1  38347