sge0sup

Description: The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0sup.x	$⊢ φ \to X \in V$
	sge0sup.f	$⊢ φ \to F : X ⟶ [0, +∞]$
Assertion	sge0sup	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		sge0sup.x	$⊢ φ \to X \in V$
2		sge0sup.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		eqidd	$⊢ (φ \land +∞ \in ran F) \to +∞ = +∞$
4	1	adantr	$⊢ (φ \land +∞ \in ran F) \to X \in V$
5	2	adantr	$⊢ (φ \land +∞ \in ran F) \to F : X ⟶ [0, +∞]$
6		simpr	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran F$
7	4 5 6	sge0pnfval	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = +∞$
8		vex	$⊢ x \in V$
9	8	a1i	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in V$
10	2	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
11		elinel1	$⊢ x \in (𝒫 X \cap Fin) \to x \in 𝒫 X$
12		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
13	11 12	syl	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
14	13	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
15	10 14	fssresd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
16	9 15	sge0xrcl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \in ℝ^{*}$
17	16	adantlr	$⊢ ((φ \land +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \in ℝ^{*}$
18	17	ralrimiva	$⊢ (φ \land +∞ \in ran F) \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{*}$
19		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) = (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
20	19	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{} \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{}$
21	18 20	syl	$⊢ (φ \land +∞ \in ran F) \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
22	2	ffnd	$⊢ φ \to F Fn X$
23		fvelrnb	$⊢ F Fn X \to (+∞ \in ran F \leftrightarrow \exists y \in X F (y) = +∞)$
24	22 23	syl	$⊢ φ \to (+∞ \in ran F \leftrightarrow \exists y \in X F (y) = +∞)$
25	24	adantr	$⊢ (φ \land +∞ \in ran F) \to (+∞ \in ran F \leftrightarrow \exists y \in X F (y) = +∞)$
26	6 25	mpbid	$⊢ (φ \land +∞ \in ran F) \to \exists y \in X F (y) = +∞$
27		snelpwi	$⊢ y \in X \to \{y\} \in 𝒫 X$
28		snfi	$⊢ \{y\} \in Fin$
29	28	a1i	$⊢ y \in X \to \{y\} \in Fin$
30	27 29	elind	$⊢ y \in X \to \{y\} \in (𝒫 X \cap Fin)$
31	30	3ad2ant2	$⊢ (φ \land y \in X \land F (y) = +∞) \to \{y\} \in (𝒫 X \cap Fin)$
32		simp2	$⊢ (φ \land y \in X \land F (y) = +∞) \to y \in X$
33	2	3ad2ant1	$⊢ (φ \land y \in X \land F (y) = +∞) \to F : X ⟶ [0, +∞]$
34	32	snssd	$⊢ (φ \land y \in X \land F (y) = +∞) \to \{y\} \subseteq X$
35	33 34	fssresd	$⊢ (φ \land y \in X \land F (y) = +∞) \to ({F ↾}_{\{y\}}) : \{y\} ⟶ [0, +∞]$
36	32 35	sge0sn	$⊢ (φ \land y \in X \land F (y) = +∞) \to sum^({F ↾}_{\{y\}}) = ({F ↾}_{\{y\}}) (y)$
37		vsnid	$⊢ y \in \{y\}$
38		fvres	$⊢ y \in \{y\} \to ({F ↾}_{\{y\}}) (y) = F (y)$
39	37 38	ax-mp	$⊢ ({F ↾}_{\{y\}}) (y) = F (y)$
40	39	a1i	$⊢ (φ \land y \in X \land F (y) = +∞) \to ({F ↾}_{\{y\}}) (y) = F (y)$
41		simp3	$⊢ (φ \land y \in X \land F (y) = +∞) \to F (y) = +∞$
42	36 40 41	3eqtrrd	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ = sum^({F ↾}_{\{y\}})$
43		reseq2	$⊢ x = \{y\} \to {F ↾}_{x} = {F ↾}_{\{y\}}$
44	43	fveq2d	$⊢ x = \{y\} \to sum^({F ↾}_{x}) = sum^({F ↾}_{\{y\}})$
45	44	rspceeqv	$⊢ (\{y\} \in (𝒫 X \cap Fin) \land +∞ = sum^({F ↾}_{\{y\}})) \to \exists x \in (𝒫 X \cap Fin) +∞ = sum^({F ↾}_{x})$
46	31 42 45	syl2anc	$⊢ (φ \land y \in X \land F (y) = +∞) \to \exists x \in (𝒫 X \cap Fin) +∞ = sum^({F ↾}_{x})$
47		pnfex	$⊢ +∞ \in V$
48	47	a1i	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ \in V$
49	19 46 48	elrnmptd	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
50	49	3exp	$⊢ φ \to (y \in X \to (F (y) = +∞ \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))))$
51	50	rexlimdv	$⊢ φ \to (\exists y \in X F (y) = +∞ \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})))$
52	51	adantr	$⊢ (φ \land +∞ \in ran F) \to (\exists y \in X F (y) = +∞ \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})))$
53	26 52	mpd	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
54		supxrpnf	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{} \land +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{} <) = +∞$
55	21 53 54	syl2anc	$⊢ (φ \land +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) = +∞$
56	3 7 55	3eqtr4d	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$
57	1	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to X \in V$
58	2	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞]$
59		simpr	$⊢ (φ \land \neg +∞ \in ran F) \to \neg +∞ \in ran F$
60	58 59	fge0iccico	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞)$
61	57 60	sge0reval	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
62		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
63	62	adantl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
64	15	adantlr	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
65		nelrnres	$⊢ \neg +∞ \in ran F \to \neg +∞ \in ran ({F ↾}_{x})$
66	65	ad2antlr	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \neg +∞ \in ran ({F ↾}_{x})$
67	64 66	fge0iccico	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞)$
68	63 67	sge0fsum	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) = \sum_{y \in x} ({F ↾}_{x}) (y)$
69		simpr	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to y \in x$
70		fvres	$⊢ y \in x \to ({F ↾}_{x}) (y) = F (y)$
71	69 70	syl	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to ({F ↾}_{x}) (y) = F (y)$
72	71	sumeq2dv	$⊢ x \in (𝒫 X \cap Fin) \to \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
73	72	adantl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} ({F ↾}_{x}) (y) = \sum_{y \in x} F (y)$
74	68 73	eqtrd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) = \sum_{y \in x} F (y)$
75	74	mpteq2dva	$⊢ (φ \land \neg +∞ \in ran F) \to (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
76	75	rneqd	$⊢ (φ \land \neg +∞ \in ran F) \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) = ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y))$
77	76	supeq1d	$⊢ (φ \land \neg +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <)$
78	61 77	eqtr4d	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$
79	56 78	pm2.61dan	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0sup

Proof