Theorem esum0

Description: Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017)

	Ref	Expression
Hypothesis	esum0.k	|- F/_ k A
Assertion	esum0	|- ( A e. V -> sum* k e. A 0 = 0 )

Proof

Step	Hyp	Ref	Expression
1		esum0.k	|- F/_ k A
2	1	nfel1	|- F/ k A e. V
3		id	|- ( A e. V -> A e. V )
4		0e0iccpnf	|- 0 e. ( 0 [,] +oo )
5	4	a1i	|- ( ( A e. V /\ k e. A ) -> 0 e. ( 0 [,] +oo ) )
6		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
7		cmnmnd	|- ( ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd -> ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd )
8	6 7	ax-mp	|- ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd
9		vex	|- x e. _V
10		xrge00	|- 0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) )
11	10	gsumz	|- ( ( ( RR*s |`s ( 0 [,] +oo ) ) e. Mnd /\ x e. _V ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> 0 ) ) = 0 )
12	8 9 11	mp2an	|- ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> 0 ) ) = 0
13	12	a1i	|- ( ( A e. V /\ x e. ( ~P A i^i Fin ) ) -> ( ( RR*s |`s ( 0 [,] +oo ) ) gsum ( k e. x |-> 0 ) ) = 0 )
14	2 1 3 5 13	esumval	|- ( A e. V -> sum* k e. A 0 = sup ( ran ( x e. ( ~P A i^i Fin ) |-> 0 ) , RR* , < ) )
15		fconstmpt	|- ( ( ~P A i^i Fin ) X. { 0 } ) = ( x e. ( ~P A i^i Fin ) |-> 0 )
16	15	eqcomi	|- ( x e. ( ~P A i^i Fin ) |-> 0 ) = ( ( ~P A i^i Fin ) X. { 0 } )
17		0xr	|- 0 e. RR*
18	17	rgenw	|- A. x e. ( ~P A i^i Fin ) 0 e. RR*
19		eqid	|- ( x e. ( ~P A i^i Fin ) |-> 0 ) = ( x e. ( ~P A i^i Fin ) |-> 0 )
20	19	fnmpt	|- ( A. x e. ( ~P A i^i Fin ) 0 e. RR* -> ( x e. ( ~P A i^i Fin ) |-> 0 ) Fn ( ~P A i^i Fin ) )
21	18 20	ax-mp	|- ( x e. ( ~P A i^i Fin ) |-> 0 ) Fn ( ~P A i^i Fin )
22		0elpw	|- (/) e. ~P A
23		0fin	|- (/) e. Fin
24		elin	|- ( (/) e. ( ~P A i^i Fin ) <-> ( (/) e. ~P A /\ (/) e. Fin ) )
25	22 23 24	mpbir2an	|- (/) e. ( ~P A i^i Fin )
26	25	ne0ii	|- ( ~P A i^i Fin ) =/= (/)
27		fconst5	|- ( ( ( x e. ( ~P A i^i Fin ) |-> 0 ) Fn ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) =/= (/) ) -> ( ( x e. ( ~P A i^i Fin ) |-> 0 ) = ( ( ~P A i^i Fin ) X. { 0 } ) <-> ran ( x e. ( ~P A i^i Fin ) |-> 0 ) = { 0 } ) )
28	21 26 27	mp2an	|- ( ( x e. ( ~P A i^i Fin ) |-> 0 ) = ( ( ~P A i^i Fin ) X. { 0 } ) <-> ran ( x e. ( ~P A i^i Fin ) |-> 0 ) = { 0 } )
29	16 28	mpbi	|- ran ( x e. ( ~P A i^i Fin ) |-> 0 ) = { 0 }
30	29	a1i	|- ( A e. V -> ran ( x e. ( ~P A i^i Fin ) |-> 0 ) = { 0 } )
31	30	supeq1d	|- ( A e. V -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> 0 ) , RR* , < ) = sup ( { 0 } , RR* , < ) )
32		xrltso	|- < Or RR*
33		supsn	|- ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
34	32 17 33	mp2an	|- sup ( { 0 } , RR* , < ) = 0
35	31 34	eqtrdi	|- ( A e. V -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> 0 ) , RR* , < ) = 0 )
36	14 35	eqtrd	|- ( A e. V -> sum* k e. A 0 = 0 )