sge0val

Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

		Ref	Expression
	Assertion	sge0val	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to sum^(F) = if (+∞ \in ran F, +∞, sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{*} <))$

Proof

Step	Hyp	Ref	Expression
1		df-sumge0	$⊢ sum^= (x \in V ⟼ if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)))$
2	1	a1i	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to sum^= (x \in V ⟼ if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)))$
3		rneq	$⊢ x = F \to ran x = ran F$
4	3	eleq2d	$⊢ x = F \to (+∞ \in ran x \leftrightarrow +∞ \in ran F)$
5	4	adantl	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to (+∞ \in ran x \leftrightarrow +∞ \in ran F)$
6		dmeq	$⊢ x = F \to dom x = dom F$
7	6	adantl	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to dom x = dom F$
8		fdm	$⊢ F : X ⟶ [0, +∞] \to dom F = X$
9	8	adantr	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to dom F = X$
10	7 9	eqtrd	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to dom x = X$
11	10	pweqd	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to 𝒫 dom x = 𝒫 X$
12	11	ineq1d	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to 𝒫 dom x \cap Fin = 𝒫 X \cap Fin$
13	12	mpteq1d	$⊢ (F : X ⟶ [0, +∞] \land x = F) \to (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} x (w))$
14	13	adantll	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} x (w))$
15		fveq1	$⊢ x = F \to x (w) = F (w)$
16	15	sumeq2sdv	$⊢ x = F \to \sum_{w \in y} x (w) = \sum_{w \in y} F (w)$
17	16	mpteq2dv	$⊢ x = F \to (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} x (w)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w))$
18	17	adantl	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} x (w)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w))$
19	14 18	eqtrd	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) = (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w))$
20	19	rneqd	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) = ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w))$
21	20	supeq1d	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{} <) = sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{} <)$
22	5 21	ifbieq2d	$⊢ ((X \in V \land F : X ⟶ [0, +∞]) \land x = F) \to if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{} <)) = if (+∞ \in ran F, +∞, sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{} <))$
23		simpr	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to F : X ⟶ [0, +∞]$
24		simpl	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to X \in V$
25		fex	$⊢ (F : X ⟶ [0, +∞] \land X \in V) \to F \in V$
26	23 24 25	syl2anc	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to F \in V$
27		pnfxr	$⊢ +∞ \in ℝ^{*}$
28	27	a1i	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to +∞ \in ℝ^{*}$
29		xrltso	$⊢ < Or ℝ^{*}$
30	29	supex	$⊢ sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{*} <) \in V$
31	30	a1i	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{*} <) \in V$
32	28 31	ifexd	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to if (+∞ \in ran F, +∞, sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{*} <)) \in V$
33	2 22 26 32	fvmptd	$⊢ (X \in V \land F : X ⟶ [0, +∞]) \to sum^(F) = if (+∞ \in ran F, +∞, sup (ran (y \in (𝒫 X \cap Fin) ⟼ \sum_{w \in y} F (w)) ℝ^{*} <))$

Metamath Proof Explorer

Theorem sge0val

Proof