Theorem sge0sn 38009

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 4659	. . . . 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 466	. . . 4 |- ( ( ph /\ ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
5		id 23	. . . . . . 7 |- ( ( F ` A ) = +oo -> ( F ` A ) = +oo )
6	5	eqcomd 2430	. . . . . 6 |- ( ( F ` A ) = +oo -> +oo = ( F ` A ) )
7	6	adantl 467	. . . . 5 |- ( ( ph /\ ( F ` A ) = +oo ) -> +oo = ( F ` A ) )
8		ffun 5745	. . . . . . . 8 |- ( F : { A } --> ( 0 [,] +oo ) -> Fun F )
9	3, 8	syl 17	. . . . . . 7 |- ( ph -> Fun F )
10	9	adantr 466	. . . . . 6 |- ( ( ph /\ ( F ` A ) = +oo ) -> Fun F )
11		sge0sn.1	. . . . . . . . 9 |- ( ph -> A e. V )
12		snidg 4022	. . . . . . . . 9 |- ( A e. V -> A e. { A } )
13	11, 12	syl 17	. . . . . . . 8 |- ( ph -> A e. { A } )
14		fdm 5747	. . . . . . . . . 10 |- ( F : { A } --> ( 0 [,] +oo ) -> dom F = { A } )
15	3, 14	syl 17	. . . . . . . . 9 |- ( ph -> dom F = { A } )
16	15	eqcomd 2430	. . . . . . . 8 |- ( ph -> { A } = dom F )
17	13, 16	eleqtrd 2512	. . . . . . 7 |- ( ph -> A e. dom F )
18	17	adantr 466	. . . . . 6 |- ( ( ph /\ ( F ` A ) = +oo ) -> A e. dom F )
19		fvelrn 6027	. . . . . 6 |- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )
20	10, 18, 19	syl2anc 665	. . . . 5 |- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) e. ran F )
21	7, 20	eqeltrd 2510	. . . 4 |- ( ( ph /\ ( F ` A ) = +oo ) -> +oo e. ran F )
22	2, 4, 21	sge0pnfval 38003	. . 3 |- ( ( ph /\ ( F ` A ) = +oo ) -> (Σ^ ` F ) = +oo )
23		simpr 462	. . 3 |- ( ( ph /\ ( F ` A ) = +oo ) -> ( F ` A ) = +oo )
24	22, 23	eqtr4d 2466	. 2 |- ( ( ph /\ ( F ` A ) = +oo ) -> (Σ^ ` F ) = ( F ` A ) )
25	1	a1i 11	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { A } e. _V )
26	3	adantr 466	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,] +oo ) )
27		elsni 4021	. . . . . . . . 9 |- ( +oo e. { ( F ` A ) } -> +oo = ( F ` A ) )
28	27	eqcomd 2430	. . . . . . . 8 |- ( +oo e. { ( F ` A ) } -> ( F ` A ) = +oo )
29	28	con3i 140	. . . . . . 7 |- ( -. ( F ` A ) = +oo -> -. +oo e. { ( F ` A ) } )
30	29	adantl 467	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. { ( F ` A ) } )
31	11, 3	rnsnf 37308	. . . . . . . 8 |- ( ph -> ran F = { ( F ` A ) } )
32	31	eqcomd 2430	. . . . . . 7 |- ( ph -> { ( F ` A ) } = ran F )
33	32	adantr 466	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { ( F ` A ) } = ran F )
34	30, 33	neleqtrd 2534	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> -. +oo e. ran F )
35	26, 34	fge0iccico 38000	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F : { A } --> ( 0 [,) +oo ) )
36	25, 35	sge0reval 38002	. . 3 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P { A } i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
37		sum0 13775	. . . . . . . 8 |- sum_ y e. (/) ( F ` y ) = 0
38	37	eqcomi 2435	. . . . . . 7 |- 0 = sum_ y e. (/) ( F ` y )
39	38	a1i 11	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> 0 = sum_ y e. (/) ( F ` y ) )
40		nfcvd 2585	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> F/_ y ( F ` A ) )
41		nfv 1751	. . . . . . . 8 |- F/ y ( ph /\ -. ( F ` A ) = +oo )
42		fveq2 5878	. . . . . . . . 9 |- ( y = A -> ( F ` y ) = ( F ` A ) )
43	42	adantl 467	. . . . . . . 8 |- ( ( ( ph /\ -. ( F ` A ) = +oo ) /\ y = A ) -> ( F ` y ) = ( F ` A ) )
44	11	adantr 466	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. V )
45		rge0ssre 11741	. . . . . . . . . 10 |- ( 0 [,) +oo ) C_ RR
46		ax-resscn 9597	. . . . . . . . . 10 |- RR C_ CC
47	45, 46	sstri 3473	. . . . . . . . 9 |- ( 0 [,) +oo ) C_ CC
48	44, 12	syl 17	. . . . . . . . . 10 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> A e. { A } )
49	35, 48	ffvelrnd 6035	. . . . . . . . 9 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. ( 0 [,) +oo ) )
50	47, 49	sseldi 3462	. . . . . . . 8 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) e. CC )
51	40, 41, 43, 44, 50	sumsnd 37208	. . . . . . 7 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> sum_ y e. { A } ( F ` y ) = ( F ` A ) )
52	51	eqcomd 2430	. . . . . 6 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sum_ y e. { A } ( F ` y ) )
53	39, 52	preq12d 4084	. . . . 5 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> { 0 , ( F ` A ) } = { sum_ y e. (/) ( F ` y ) , sum_ y e. { A } ( F ` y ) } )
54	53	supeq1d 7963	. . . 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 11441	. . . . . . . 8 |- < Or RR*
56	55	a1i 11	. . . . . . 7 |- ( ph -> < Or RR* )
57		0xr 9688	. . . . . . . 8 |- 0 e. RR*
58	57	a1i 11	. . . . . . 7 |- ( ph -> 0 e. RR* )
59		iccssxr 11718	. . . . . . . 8 |- ( 0 [,] +oo ) C_ RR*
60	3, 13	ffvelrnd 6035	. . . . . . . 8 |- ( ph -> ( F ` A ) e. ( 0 [,] +oo ) )
61	59, 60	sseldi 3462	. . . . . . 7 |- ( ph -> ( F ` A ) e. RR* )
62		suppr 7990	. . . . . . 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 1264	. . . . . 6 |- ( ph -> sup ( { 0 , ( F ` A ) } , RR* , < ) = if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) )
64		pnfxr 11413	. . . . . . . . . . 11 |- +oo e. RR*
65	64	a1i 11	. . . . . . . . . 10 |- ( ph -> +oo e. RR* )
66	58, 65, 60	3jca 1185	. . . . . . . . 9 |- ( ph -> ( 0 e. RR* /\ +oo e. RR* /\ ( F ` A ) e. ( 0 [,] +oo ) ) )
67		iccgelb 11692	. . . . . . . . 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 9701	. . . . . . . 8 |- ( ph -> ( 0 <_ ( F ` A ) <-> -. ( F ` A ) < 0 ) )
70	68, 69	mpbid 213	. . . . . . 7 |- ( ph -> -. ( F ` A ) < 0 )
71	70	iffalsed 3920	. . . . . 6 |- ( ph -> if ( ( F ` A ) < 0 , 0 , ( F ` A ) ) = ( F ` A ) )
72	63, 71	eqtr2d 2464	. . . . 5 |- ( ph -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
73	72	adantr 466	. . . 4 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> ( F ` A ) = sup ( { 0 , ( F ` A ) } , RR* , < ) )
74		pwsn 4210	. . . . . . . . . . . 12 |- ~P { A } = { (/) , { A } }
75	74	ineq1i 3660	. . . . . . . . . . 11 |- ( ~P { A } i^i Fin ) = ( { (/) , { A } } i^i Fin )
76		0fin 7802	. . . . . . . . . . . . 13 |- (/) e. Fin
77		snfi 7654	. . . . . . . . . . . . 13 |- { A } e. Fin
78		prssi 4153	. . . . . . . . . . . . 13 |- ( ( (/) e. Fin /\ { A } e. Fin ) -> { (/) , { A } } C_ Fin )
79	76, 77, 78	mp2an 676	. . . . . . . . . . . 12 |- { (/) , { A } } C_ Fin
80		df-ss 3450	. . . . . . . . . . . . 13 |- ( { (/) , { A } } C_ Fin <-> ( { (/) , { A } } i^i Fin ) = { (/) , { A } } )
81	80	biimpi 197	. . . . . . . . . . . 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 2451	. . . . . . . . . 10 |- ( ~P { A } i^i Fin ) = { (/) , { A } }
84		mpteq1 4501	. . . . . . . . . 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 4553	. . . . . . . . . . . . 13 |- (/) e. _V
87	86	a1i 11	. . . . . . . . . . . 12 |- ( T. -> (/) e. _V )
88	1	a1i 11	. . . . . . . . . . . 12 |- ( T. -> { A } e. _V )
89		sumex 13742	. . . . . . . . . . . . 13 |- sum_ y e. (/) ( F ` y ) e. _V
90	89	a1i 11	. . . . . . . . . . . 12 |- ( T. -> sum_ y e. (/) ( F ` y ) e. _V )
91		sumex 13742	. . . . . . . . . . . . 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 13743	. . . . . . . . . . . . 13 |- ( x = (/) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
94	93	adantl 467	. . . . . . . . . . . 12 |- ( ( T. /\ x = (/) ) -> sum_ y e. x ( F ` y ) = sum_ y e. (/) ( F ` y ) )
95		sumeq1 13743	. . . . . . . . . . . . 13 |- ( x = { A } -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
96	95	adantl 467	. . . . . . . . . . . 12 |- ( ( T. /\ x = { A } ) -> sum_ y e. x ( F ` y ) = sum_ y e. { A } ( F ` y ) )
97	87, 88, 90, 92, 94, 96	fmptpr 6101	. . . . . . . . . . 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 1446	. . . . . . . . . 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 2435	. . . . . . . . 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 2451	. . . . . . . 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 5077	. . . . . . 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 5332	. . . . . . . 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 676	. . . . . . 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 2451	. . . . . 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 7964	. . . . 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 2473	. . 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 2466	. 2 |- ( ( ph /\ -. ( F ` A ) = +oo ) -> (Σ^ ` F ) = ( F ` A ) )
109	24, 108	pm2.61dan 798	1 |- ( ph -> (Σ^ ` F ) = ( F ` A ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   T. wtru 1438   e. wcel 1868   _Vcvv 3081   i^i cin 3435   C_ wss 3436   (/)c0 3761   ifcif 3909   ~Pcpw 3979   {csn 3996   {cpr 3998   <.cop 4002   class class class wbr 4420   |-> cmpt 4479   Or wor 4770   dom cdm 4850   ran crn 4851   Fun wfun 5592   -->wf 5594   ` cfv 5598  (class class class)co 6302   Fincfn 7574   supcsup 7957   CCcc 9538   RRcr 9539   0cc0 9540   +oocpnf 9673   RR*cxr 9675   < clt 9676   <_ cle 9677   [,)cico 11638   [,]cicc 11639   sum_csu 13740  Σ^{^}csumge0 37992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-inf2 8149  ax-cnex 9596  ax-resscn 9597  ax-1cn 9598  ax-icn 9599  ax-addcl 9600  ax-addrcl 9601  ax-mulcl 9602  ax-mulrcl 9603  ax-mulcom 9604  ax-addass 9605  ax-mulass 9606  ax-distr 9607  ax-i2m1 9608  ax-1ne0 9609  ax-1rid 9610  ax-rnegex 9611  ax-rrecex 9612  ax-cnre 9613  ax-pre-lttri 9614  ax-pre-lttrn 9615  ax-pre-ltadd 9616  ax-pre-mulgt0 9617  ax-pre-sup 9618

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-nel 2621  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-se 4810  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-isom 5607  df-riota 6264  df-ov 6305  df-oprab 6306  df-mpt2 6307  df-om 6704  df-1st 6804  df-2nd 6805  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-1o 7187  df-oadd 7191  df-er 7368  df-en 7575  df-dom 7576  df-sdom 7577  df-fin 7578  df-sup 7959  df-oi 8028  df-card 8375  df-pnf 9678  df-mnf 9679  df-xr 9680  df-ltxr 9681  df-le 9682  df-sub 9863  df-neg 9864  df-div 10271  df-nn 10611  df-2 10669  df-3 10670  df-n0 10871  df-z 10939  df-uz 11161  df-rp 11304  df-ico 11642  df-icc 11643  df-fz 11786  df-fzo 11917  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13151  df-re 13152  df-im 13153  df-sqrt 13287  df-abs 13288  df-clim 13540  df-sum 13741  df-sumge0 37993

This theorem is referenced by:  sge0snmpt  38013  sge0sup  38021  caratheodorylem1  38126