sge0fsum

Description: The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0fsum.x	$⊢ φ \to X \in Fin$
	sge0fsum.f	$⊢ φ \to F : X ⟶ [0, +∞)$
Assertion	sge0fsum	$⊢ φ \to sum^(F) = \sum_{x \in X} F (x)$

Proof

Step	Hyp	Ref	Expression
1		sge0fsum.x	$⊢ φ \to X \in Fin$
2		sge0fsum.f	$⊢ φ \to F : X ⟶ [0, +∞)$
3	2	fge0icoicc	$⊢ φ \to F : X ⟶ [0, +∞]$
4	1 3	sge0xrcl	$⊢ φ \to sum^(F) \in ℝ^{*}$
5		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
6	2	ffvelcdmda	$⊢ (φ \land x \in X) \to F (x) \in [0, +∞)$
7	5 6	sselid	$⊢ (φ \land x \in X) \to F (x) \in ℝ$
8	1 7	fsumrecl	$⊢ φ \to \sum_{x \in X} F (x) \in ℝ$
9	8	rexrd	$⊢ φ \to \sum_{x \in X} F (x) \in ℝ^{*}$
10	1 2	sge0reval	$⊢ φ \to sum^(F) = sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) ℝ^{*} <)$
11		simpr	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))$
12		vex	$⊢ w \in V$
13	12	a1i	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to w \in V$
14		eqid	$⊢ (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))$
15	14	elrnmpt	$⊢ w \in V \to (w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) \leftrightarrow \exists y \in (𝒫 X \cap Fin) w = \sum_{x \in y} F (x))$
16	13 15	syl	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to (w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) \leftrightarrow \exists y \in (𝒫 X \cap Fin) w = \sum_{x \in y} F (x))$
17	11 16	mpbid	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to \exists y \in (𝒫 X \cap Fin) w = \sum_{x \in y} F (x)$
18		simp3	$⊢ (φ \land y \in (𝒫 X \cap Fin) \land w = \sum_{x \in y} F (x)) \to w = \sum_{x \in y} F (x)$
19	1	adantr	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to X \in Fin$
20	2	fge0npnf	$⊢ φ \to \neg +∞ \in ran F$
21	3 20	fge0iccre	$⊢ φ \to F : X ⟶ ℝ$
22	21	adantr	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to F : X ⟶ ℝ$
23	22	adantr	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to F : X ⟶ ℝ$
24		simpr	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to x \in X$
25	23 24	ffvelcdmd	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to F (x) \in ℝ$
26		0xr	$⊢ 0 \in ℝ^{*}$
27	26	a1i	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to 0 \in ℝ^{*}$
28		pnfxr	$⊢ +∞ \in ℝ^{*}$
29	28	a1i	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to +∞ \in ℝ^{*}$
30	3	adantr	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
31	30	ffvelcdmda	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to F (x) \in [0, +∞]$
32		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (x) \in [0, +∞]) \to 0 \leq F (x)$
33	27 29 31 32	syl3anc	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in X) \to 0 \leq F (x)$
34		elinel1	$⊢ y \in (𝒫 X \cap Fin) \to y \in 𝒫 X$
35		elpwi	$⊢ y \in 𝒫 X \to y \subseteq X$
36	34 35	syl	$⊢ y \in (𝒫 X \cap Fin) \to y \subseteq X$
37	36	adantl	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to y \subseteq X$
38	19 25 33 37	fsumless	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} F (x) \leq \sum_{x \in X} F (x)$
39	38	3adant3	$⊢ (φ \land y \in (𝒫 X \cap Fin) \land w = \sum_{x \in y} F (x)) \to \sum_{x \in y} F (x) \leq \sum_{x \in X} F (x)$
40	18 39	eqbrtrd	$⊢ (φ \land y \in (𝒫 X \cap Fin) \land w = \sum_{x \in y} F (x)) \to w \leq \sum_{x \in X} F (x)$
41	40	3exp	$⊢ φ \to (y \in (𝒫 X \cap Fin) \to (w = \sum_{x \in y} F (x) \to w \leq \sum_{x \in X} F (x)))$
42	41	rexlimdv	$⊢ φ \to (\exists y \in (𝒫 X \cap Fin) w = \sum_{x \in y} F (x) \to w \leq \sum_{x \in X} F (x))$
43	42	adantr	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to (\exists y \in (𝒫 X \cap Fin) w = \sum_{x \in y} F (x) \to w \leq \sum_{x \in X} F (x))$
44	17 43	mpd	$⊢ (φ \land w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x))) \to w \leq \sum_{x \in X} F (x)$
45	44	ralrimiva	$⊢ φ \to \forall w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) w \leq \sum_{x \in X} F (x)$
46		elinel2	$⊢ y \in (𝒫 X \cap Fin) \to y \in Fin$
47	46	adantl	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to y \in Fin$
48	22	adantr	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in y) \to F : X ⟶ ℝ$
49	37	sselda	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in y) \to x \in X$
50	48 49	ffvelcdmd	$⊢ ((φ \land y \in (𝒫 X \cap Fin)) \land x \in y) \to F (x) \in ℝ$
51	47 50	fsumrecl	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} F (x) \in ℝ$
52	51	rexrd	$⊢ (φ \land y \in (𝒫 X \cap Fin)) \to \sum_{x \in y} F (x) \in ℝ^{*}$
53	52	ralrimiva	$⊢ φ \to \forall y \in (𝒫 X \cap Fin) \sum_{x \in y} F (x) \in ℝ^{*}$
54	14	rnmptss	$⊢ \forall y \in (𝒫 X \cap Fin) \sum_{x \in y} F (x) \in ℝ^{} \to ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) \subseteq ℝ^{}$
55	53 54	syl	$⊢ φ \to ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) \subseteq ℝ^{*}$
56		supxrleub	$⊢ (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) \subseteq ℝ^{} \land \sum_{x \in X} F (x) \in ℝ^{}) \to (sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) ℝ^{*} <) \leq \sum_{x \in X} F (x) \leftrightarrow \forall w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) w \leq \sum_{x \in X} F (x))$
57	55 9 56	syl2anc	$⊢ φ \to (sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) ℝ^{*} <) \leq \sum_{x \in X} F (x) \leftrightarrow \forall w \in ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) w \leq \sum_{x \in X} F (x))$
58	45 57	mpbird	$⊢ φ \to sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{x \in y} F (x)) ℝ^{*} <) \leq \sum_{x \in X} F (x)$
59	10 58	eqbrtrd	$⊢ φ \to sum^(F) \leq \sum_{x \in X} F (x)$
60		ssid	$⊢ X \subseteq X$
61	60	a1i	$⊢ φ \to X \subseteq X$
62	1 2 61 1	fsumlesge0	$⊢ φ \to \sum_{x \in X} F (x) \leq sum^(F)$
63	4 9 59 62	xrletrid	$⊢ φ \to sum^(F) = \sum_{x \in X} F (x)$

Metamath Proof Explorer

Theorem sge0fsum

Proof