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	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
	xrge0gsumle.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	xrge0gsumle.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
	xrge0gsumle.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) )
	xrge0gsumle.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
Assertion	xrge0gsumle	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ≤ ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrge0gsumle.g	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		xrge0gsumle.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		xrge0gsumle.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
4		xrge0gsumle.b	⊢ ( 𝜑 → 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) )
5		xrge0gsumle.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
6		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
7		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
8	1 7	ressbas2	⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( 0 [,] +∞ ) = ( Base ‘ 𝐺 ) )
9	6 8	ax-mp	⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
10		eqid	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
11	10	xrge0subm	⊢ ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
12		xrex	⊢ ℝ* ∈ V
13	12	difexi	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
14		simpl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ∈ ℝ* )
15		ge0nemnf	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → 𝑥 ≠ -∞ )
16	14 15	jca	⊢ ( ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
17		elxrge0	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 0 ≤ 𝑥 ) )
18		eldifsn	⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≠ -∞ ) )
19	16 17 18	3imtr4i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ( ℝ* ∖ { -∞ } ) )
20	19	ssriv	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
21		ressabs	⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
22	13 20 21	mp2an	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
23	1 22	eqtr4i	⊢ 𝐺 = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
24	10	xrs10	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
25	23 24	subm0	⊢ ( ( 0 [,] +∞ ) ∈ ( SubMnd ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) → 0 = ( 0g ‘ 𝐺 ) )
26	11 25	ax-mp	⊢ 0 = ( 0g ‘ 𝐺 )
27		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
28	1 27	eqeltri	⊢ 𝐺 ∈ CMnd
29	28	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
30		elfpw	⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑠 ⊆ 𝐴 ∧ 𝑠 ∈ Fin ) )
31	30	simprbi	⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑠 ∈ Fin )
32	31	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑠 ∈ Fin )
33	30	simplbi	⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑠 ⊆ 𝐴 )
34		fssres	⊢ ( ( 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ∧ 𝑠 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝑠 ) : 𝑠 ⟶ ( 0 [,] +∞ ) )
35	3 33 34	syl2an	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑠 ) : 𝑠 ⟶ ( 0 [,] +∞ ) )
36		c0ex	⊢ 0 ∈ V
37	36	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ V )
38	35 32 37	fdmfifsupp	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑠 ) finSupp 0 )
39	9 26 29 32 35 38	gsumcl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ∈ ( 0 [,] +∞ ) )
40	6 39	sselid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ∈ ℝ* )
41	40	fmpttd	⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ ℝ* )
42	41	frnd	⊢ ( 𝜑 → ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) ⊆ ℝ* )
43		0ss	⊢ ∅ ⊆ 𝐴
44		0fi	⊢ ∅ ∈ Fin
45		elfpw	⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ∈ Fin ) )
46	43 44 45	mpbir2an	⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
47		0cn	⊢ 0 ∈ ℂ
48		eqid	⊢ ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) = ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) )
49		reseq2	⊢ ( 𝑠 = ∅ → ( 𝐹 ↾ 𝑠 ) = ( 𝐹 ↾ ∅ ) )
50		res0	⊢ ( 𝐹 ↾ ∅ ) = ∅
51	49 50	eqtrdi	⊢ ( 𝑠 = ∅ → ( 𝐹 ↾ 𝑠 ) = ∅ )
52	51	oveq2d	⊢ ( 𝑠 = ∅ → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) = ( 𝐺 Σg ∅ ) )
53	26	gsum0	⊢ ( 𝐺 Σg ∅ ) = 0
54	52 53	eqtrdi	⊢ ( 𝑠 = ∅ → ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) = 0 )
55	48 54	elrnmpt1s	⊢ ( ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ 0 ∈ ℂ ) → 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) )
56	46 47 55	mp2an	⊢ 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) )
57	56	a1i	⊢ ( 𝜑 → 0 ∈ ran ( 𝑠 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑠 ) ) ) )
58	42 57	sseldd	⊢ ( 𝜑 → 0 ∈ ℝ* )
59	28	a1i	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
60	4	elin2d	⊢ ( 𝜑 → 𝐵 ∈ Fin )
61		diffi	⊢ ( 𝐵 ∈ Fin → ( 𝐵 ∖ 𝐶 ) ∈ Fin )
62	60 61	syl	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐶 ) ∈ Fin )
63		elfpw	⊢ ( 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐵 ∈ Fin ) )
64	63	simplbi	⊢ ( 𝐵 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝐵 ⊆ 𝐴 )
65	4 64	syl	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
66	65	ssdifssd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐶 ) ⊆ 𝐴 )
67	3 66	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) : ( 𝐵 ∖ 𝐶 ) ⟶ ( 0 [,] +∞ ) )
68	36	a1i	⊢ ( 𝜑 → 0 ∈ V )
69	67 62 68	fdmfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) finSupp 0 )
70	9 26 59 62 67 69	gsumcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) )
71	6 70	sselid	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* )
72	60 5	ssfid	⊢ ( 𝜑 → 𝐶 ∈ Fin )
73	5 65	sstrd	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
74	3 73	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ( 0 [,] +∞ ) )
75	74 72 68	fdmfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) finSupp 0 )
76	9 26 59 72 74 75	gsumcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
77	6 76	sselid	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ℝ* )
78		elxrge0	⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* ∧ 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
79	78	simprbi	⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
80	70 79	syl	⊢ ( 𝜑 → 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
81		xleadd2a	⊢ ( ( ( 0 ∈ ℝ* ∧ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ∈ ℝ* ∧ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ∈ ℝ* ) ∧ 0 ≤ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e 0 ) ≤ ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
82	58 71 77 80 81	syl31anc	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e 0 ) ≤ ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
83	77	xaddridd	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e 0 ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) )
84		ovex	⊢ ( 0 [,] +∞ ) ∈ V
85		xrsadd	⊢ +e = ( +g ‘ ℝ*𝑠 )
86	1 85	ressplusg	⊢ ( ( 0 [,] +∞ ) ∈ V → +e = ( +g ‘ 𝐺 ) )
87	84 86	ax-mp	⊢ +e = ( +g ‘ 𝐺 )
88	3 65	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ ( 0 [,] +∞ ) )
89	88 60 68	fdmfifsupp	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) finSupp 0 )
90		disjdif	⊢ ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅
91	90	a1i	⊢ ( 𝜑 → ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ )
92		undif2	⊢ ( 𝐶 ∪ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐶 ∪ 𝐵 )
93		ssequn1	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐶 ∪ 𝐵 ) = 𝐵 )
94	5 93	sylib	⊢ ( 𝜑 → ( 𝐶 ∪ 𝐵 ) = 𝐵 )
95	92 94	eqtr2id	⊢ ( 𝜑 → 𝐵 = ( 𝐶 ∪ ( 𝐵 ∖ 𝐶 ) ) )
96	9 26 87 59 4 88 89 91 95	gsumsplit	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) = ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) +e ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
97	5	resabs1d	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) = ( 𝐹 ↾ 𝐶 ) )
98	97	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) )
99		difss	⊢ ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵
100		resabs1	⊢ ( ( 𝐵 ∖ 𝐶 ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) )
101	99 100	mp1i	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) )
102	101	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) )
103	98 102	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ 𝐶 ) ) +e ( 𝐺 Σg ( ( 𝐹 ↾ 𝐵 ) ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) )
104	96 103	eqtr2d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) +e ( 𝐺 Σg ( 𝐹 ↾ ( 𝐵 ∖ 𝐶 ) ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )
105	82 83 104	3brtr3d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ≤ ( 𝐺 Σg ( 𝐹 ↾ 𝐵 ) ) )