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 = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
	xrge0gsumle.a	$⊢ φ \to A \in V$
	xrge0gsumle.f	$⊢ φ \to F : A ⟶ [0, +∞]$
	xrge0gsumle.b	$⊢ φ \to B \in (𝒫 A \cap Fin)$
	xrge0gsumle.c	$⊢ φ \to C \subseteq B$
Assertion	xrge0gsumle	$⊢ φ \to \sum_{G} ({F ↾}_{C}) \leq \sum_{G} ({F ↾}_{B})$

Proof

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

Metamath Proof Explorer

Theorem xrge0gsumle

Proof