Theorem sge0z

Description: Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0z.1	|- F/ k ph
	sge0z.2	|- ( ph -> A e. V )
Assertion	sge0z	|- ( ph -> ( sum^ ` ( k e. A |-> 0 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		sge0z.1	|- F/ k ph
2		sge0z.2	|- ( ph -> A e. V )
3		0e0icopnf	|- 0 e. ( 0 [,) +oo )
4	3	a1i	|- ( ( ph /\ k e. A ) -> 0 e. ( 0 [,) +oo ) )
5	1 4	fmptd2f	|- ( ph -> ( k e. A |-> 0 ) : A --> ( 0 [,) +oo ) )
6	2 5	sge0reval	|- ( ph -> ( sum^ ` ( k e. A |-> 0 ) ) = sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) ) , RR* , < ) )
7		eqidd	|- ( ( x e. ( ~P A i^i Fin ) /\ y e. x ) -> ( k e. A |-> 0 ) = ( k e. A |-> 0 ) )
8		eqidd	|- ( ( ( x e. ( ~P A i^i Fin ) /\ y e. x ) /\ k = y ) -> 0 = 0 )
9		elpwinss	|- ( x e. ( ~P A i^i Fin ) -> x C_ A )
10	9	sselda	|- ( ( x e. ( ~P A i^i Fin ) /\ y e. x ) -> y e. A )
11		0cnd	|- ( ( x e. ( ~P A i^i Fin ) /\ y e. x ) -> 0 e. CC )
12	7 8 10 11	fvmptd	|- ( ( x e. ( ~P A i^i Fin ) /\ y e. x ) -> ( ( k e. A |-> 0 ) ` y ) = 0 )
13	12	adantll	|- ( ( ( ph /\ x e. ( ~P A i^i Fin ) ) /\ y e. x ) -> ( ( k e. A |-> 0 ) ` y ) = 0 )
14	13	sumeq2dv	|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) = sum_ y e. x 0 )
15		elinel2	|- ( x e. ( ~P A i^i Fin ) -> x e. Fin )
16		olc	|- ( x e. Fin -> ( x C_ ( ZZ>= ` B ) \/ x e. Fin ) )
17		sumz	|- ( ( x C_ ( ZZ>= ` B ) \/ x e. Fin ) -> sum_ y e. x 0 = 0 )
18	15 16 17	3syl	|- ( x e. ( ~P A i^i Fin ) -> sum_ y e. x 0 = 0 )
19	18	adantl	|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ y e. x 0 = 0 )
20	14 19	eqtrd	|- ( ( ph /\ x e. ( ~P A i^i Fin ) ) -> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) = 0 )
21	20	mpteq2dva	|- ( ph -> ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) ) = ( x e. ( ~P A i^i Fin ) |-> 0 ) )
22	21	rneqd	|- ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) ) = ran ( x e. ( ~P A i^i Fin ) |-> 0 ) )
23		eqid	|- ( x e. ( ~P A i^i Fin ) |-> 0 ) = ( x e. ( ~P A i^i Fin ) |-> 0 )
24		pwfin0	|- ( ~P A i^i Fin ) =/= (/)
25	24	a1i	|- ( ph -> ( ~P A i^i Fin ) =/= (/) )
26	23 25	rnmptc	|- ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> 0 ) = { 0 } )
27	22 26	eqtrd	|- ( ph -> ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) ) = { 0 } )
28	27	supeq1d	|- ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ y e. x ( ( k e. A |-> 0 ) ` y ) ) , RR* , < ) = sup ( { 0 } , RR* , < ) )
29		xrltso	|- < Or RR*
30	29	a1i	|- ( ph -> < Or RR* )
31		0xr	|- 0 e. RR*
32		supsn	|- ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 )
33	30 31 32	sylancl	|- ( ph -> sup ( { 0 } , RR* , < ) = 0 )
34	6 28 33	3eqtrd	|- ( ph -> ( sum^ ` ( k e. A |-> 0 ) ) = 0 )