Theorem xrge0gsumle

Description: A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015)

	Ref	Expression
Hypotheses	xrge0gsumle.g	|- G = ( RR*s |`s ( 0 [,] +oo ) )
	xrge0gsumle.a	|- ( ph -> A e. V )
	xrge0gsumle.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
	xrge0gsumle.b	|- ( ph -> B e. ( ~P A i^i Fin ) )
	xrge0gsumle.c	|- ( ph -> C C_ B )
Assertion	xrge0gsumle	|- ( ph -> ( G gsum ( F |` C ) ) <_ ( G gsum ( F |` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0gsumle.g	|- G = ( RR*s |`s ( 0 [,] +oo ) )
2		xrge0gsumle.a	|- ( ph -> A e. V )
3		xrge0gsumle.f	|- ( ph -> F : A --> ( 0 [,] +oo ) )
4		xrge0gsumle.b	|- ( ph -> B e. ( ~P A i^i Fin ) )
5		xrge0gsumle.c	|- ( ph -> C C_ B )
6		iccssxr	|- ( 0 [,] +oo ) C_ RR*
7		xrsbas	|- RR* = ( Base ` RR*s )
8	1 7	ressbas2	|- ( ( 0 [,] +oo ) C_ RR* -> ( 0 [,] +oo ) = ( Base ` G ) )
9	6 8	ax-mp	|- ( 0 [,] +oo ) = ( Base ` G )
10		eqid	|- ( RR*s |`s ( RR* \ { -oo } ) ) = ( RR*s |`s ( RR* \ { -oo } ) )
11	10	xrge0subm	|- ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) )
12		xrex	|- RR* e. _V
13	12	difexi	|- ( RR* \ { -oo } ) e. _V
14		simpl	|- ( ( x e. RR* /\ 0 <_ x ) -> x e. RR* )
15		ge0nemnf	|- ( ( x e. RR* /\ 0 <_ x ) -> x =/= -oo )
16	14 15	jca	|- ( ( x e. RR* /\ 0 <_ x ) -> ( x e. RR* /\ x =/= -oo ) )
17		elxrge0	|- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
18		eldifsn	|- ( x e. ( RR* \ { -oo } ) <-> ( x e. RR* /\ x =/= -oo ) )
19	16 17 18	3imtr4i	|- ( x e. ( 0 [,] +oo ) -> x e. ( RR* \ { -oo } ) )
20	19	ssriv	|- ( 0 [,] +oo ) C_ ( RR* \ { -oo } )
21		ressabs	|- ( ( ( RR* \ { -oo } ) e. _V /\ ( 0 [,] +oo ) C_ ( RR* \ { -oo } ) ) -> ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) )
22	13 20 21	mp2an	|- ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) )
23	1 22	eqtr4i	|- G = ( ( RR*s |`s ( RR* \ { -oo } ) ) |`s ( 0 [,] +oo ) )
24	10	xrs10	|- 0 = ( 0g ` ( RR*s |`s ( RR* \ { -oo } ) ) )
25	23 24	subm0	|- ( ( 0 [,] +oo ) e. ( SubMnd ` ( RR*s |`s ( RR* \ { -oo } ) ) ) -> 0 = ( 0g ` G ) )
26	11 25	ax-mp	|- 0 = ( 0g ` G )
27		xrge0cmn	|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
28	1 27	eqeltri	|- G e. CMnd
29	28	a1i	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> G e. CMnd )
30		elfpw	|- ( s e. ( ~P A i^i Fin ) <-> ( s C_ A /\ s e. Fin ) )
31	30	simprbi	|- ( s e. ( ~P A i^i Fin ) -> s e. Fin )
32	31	adantl	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> s e. Fin )
33	30	simplbi	|- ( s e. ( ~P A i^i Fin ) -> s C_ A )
34		fssres	|- ( ( F : A --> ( 0 [,] +oo ) /\ s C_ A ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
35	3 33 34	syl2an	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) : s --> ( 0 [,] +oo ) )
36		c0ex	|- 0 e. _V
37	36	a1i	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> 0 e. _V )
38	35 32 37	fdmfifsupp	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( F |` s ) finSupp 0 )
39	9 26 29 32 35 38	gsumcl	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. ( 0 [,] +oo ) )
40	6 39	sseldi	|- ( ( ph /\ s e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` s ) ) e. RR* )
41	40	fmpttd	|- ( ph -> ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) : ( ~P A i^i Fin ) --> RR* )
42	41	frnd	|- ( ph -> ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) C_ RR* )
43		0ss	|- (/) C_ A
44		0fin	|- (/) e. Fin
45		elfpw	|- ( (/) e. ( ~P A i^i Fin ) <-> ( (/) C_ A /\ (/) e. Fin ) )
46	43 44 45	mpbir2an	|- (/) e. ( ~P A i^i Fin )
47		0cn	|- 0 e. CC
48		eqid	|- ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) = ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
49		reseq2	|- ( s = (/) -> ( F |` s ) = ( F |` (/) ) )
50		res0	|- ( F |` (/) ) = (/)
51	49 50	eqtrdi	|- ( s = (/) -> ( F |` s ) = (/) )
52	51	oveq2d	|- ( s = (/) -> ( G gsum ( F |` s ) ) = ( G gsum (/) ) )
53	26	gsum0	|- ( G gsum (/) ) = 0
54	52 53	eqtrdi	|- ( s = (/) -> ( G gsum ( F |` s ) ) = 0 )
55	48 54	elrnmpt1s	|- ( ( (/) e. ( ~P A i^i Fin ) /\ 0 e. CC ) -> 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
56	46 47 55	mp2an	|- 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) )
57	56	a1i	|- ( ph -> 0 e. ran ( s e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` s ) ) ) )
58	42 57	sseldd	|- ( ph -> 0 e. RR* )
59	28	a1i	|- ( ph -> G e. CMnd )
60	4	elin2d	|- ( ph -> B e. Fin )
61		diffi	|- ( B e. Fin -> ( B \ C ) e. Fin )
62	60 61	syl	|- ( ph -> ( B \ C ) e. Fin )
63		elfpw	|- ( B e. ( ~P A i^i Fin ) <-> ( B C_ A /\ B e. Fin ) )
64	63	simplbi	|- ( B e. ( ~P A i^i Fin ) -> B C_ A )
65	4 64	syl	|- ( ph -> B C_ A )
66	65	ssdifssd	|- ( ph -> ( B \ C ) C_ A )
67	3 66	fssresd	|- ( ph -> ( F |` ( B \ C ) ) : ( B \ C ) --> ( 0 [,] +oo ) )
68	36	a1i	|- ( ph -> 0 e. _V )
69	67 62 68	fdmfifsupp	|- ( ph -> ( F |` ( B \ C ) ) finSupp 0 )
70	9 26 59 62 67 69	gsumcl	|- ( ph -> ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) )
71	6 70	sseldi	|- ( ph -> ( G gsum ( F |` ( B \ C ) ) ) e. RR* )
72	60 5	ssfid	|- ( ph -> C e. Fin )
73	5 65	sstrd	|- ( ph -> C C_ A )
74	3 73	fssresd	|- ( ph -> ( F |` C ) : C --> ( 0 [,] +oo ) )
75	74 72 68	fdmfifsupp	|- ( ph -> ( F |` C ) finSupp 0 )
76	9 26 59 72 74 75	gsumcl	|- ( ph -> ( G gsum ( F |` C ) ) e. ( 0 [,] +oo ) )
77	6 76	sseldi	|- ( ph -> ( G gsum ( F |` C ) ) e. RR* )
78		elxrge0	|- ( ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) <-> ( ( G gsum ( F |` ( B \ C ) ) ) e. RR* /\ 0 <_ ( G gsum ( F |` ( B \ C ) ) ) ) )
79	78	simprbi	|- ( ( G gsum ( F |` ( B \ C ) ) ) e. ( 0 [,] +oo ) -> 0 <_ ( G gsum ( F |` ( B \ C ) ) ) )
80	70 79	syl	|- ( ph -> 0 <_ ( G gsum ( F |` ( B \ C ) ) ) )
81		xleadd2a	|- ( ( ( 0 e. RR* /\ ( G gsum ( F |` ( B \ C ) ) ) e. RR* /\ ( G gsum ( F |` C ) ) e. RR* ) /\ 0 <_ ( G gsum ( F |` ( B \ C ) ) ) ) -> ( ( G gsum ( F |` C ) ) +e 0 ) <_ ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
82	58 71 77 80 81	syl31anc	|- ( ph -> ( ( G gsum ( F |` C ) ) +e 0 ) <_ ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
83	77	xaddid1d	|- ( ph -> ( ( G gsum ( F |` C ) ) +e 0 ) = ( G gsum ( F |` C ) ) )
84		ovex	|- ( 0 [,] +oo ) e. _V
85		xrsadd	|- +e = ( +g ` RR*s )
86	1 85	ressplusg	|- ( ( 0 [,] +oo ) e. _V -> +e = ( +g ` G ) )
87	84 86	ax-mp	|- +e = ( +g ` G )
88	3 65	fssresd	|- ( ph -> ( F |` B ) : B --> ( 0 [,] +oo ) )
89	88 60 68	fdmfifsupp	|- ( ph -> ( F |` B ) finSupp 0 )
90		disjdif	|- ( C i^i ( B \ C ) ) = (/)
91	90	a1i	|- ( ph -> ( C i^i ( B \ C ) ) = (/) )
92		undif2	|- ( C u. ( B \ C ) ) = ( C u. B )
93		ssequn1	|- ( C C_ B <-> ( C u. B ) = B )
94	5 93	sylib	|- ( ph -> ( C u. B ) = B )
95	92 94	syl5req	|- ( ph -> B = ( C u. ( B \ C ) ) )
96	9 26 87 59 4 88 89 91 95	gsumsplit	|- ( ph -> ( G gsum ( F |` B ) ) = ( ( G gsum ( ( F |` B ) |` C ) ) +e ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) ) )
97	5	resabs1d	|- ( ph -> ( ( F |` B ) |` C ) = ( F |` C ) )
98	97	oveq2d	|- ( ph -> ( G gsum ( ( F |` B ) |` C ) ) = ( G gsum ( F |` C ) ) )
99		difss	|- ( B \ C ) C_ B
100		resabs1	|- ( ( B \ C ) C_ B -> ( ( F |` B ) |` ( B \ C ) ) = ( F |` ( B \ C ) ) )
101	99 100	mp1i	|- ( ph -> ( ( F |` B ) |` ( B \ C ) ) = ( F |` ( B \ C ) ) )
102	101	oveq2d	|- ( ph -> ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) = ( G gsum ( F |` ( B \ C ) ) ) )
103	98 102	oveq12d	|- ( ph -> ( ( G gsum ( ( F |` B ) |` C ) ) +e ( G gsum ( ( F |` B ) |` ( B \ C ) ) ) ) = ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) )
104	96 103	eqtr2d	|- ( ph -> ( ( G gsum ( F |` C ) ) +e ( G gsum ( F |` ( B \ C ) ) ) ) = ( G gsum ( F |` B ) ) )
105	82 83 104	3brtr3d	|- ( ph -> ( G gsum ( F |` C ) ) <_ ( G gsum ( F |` B ) ) )