sge0revalmpt

Description: Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0revalmpt.1	$⊢ Ⅎ x φ$
	sge0revalmpt.2	$⊢ φ \to A \in V$
	sge0revalmpt.3	$⊢ (φ \land x \in A) \to B \in [0, +∞)$
Assertion	sge0revalmpt	$⊢ φ \to sum^((x \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{x \in y} B) ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		sge0revalmpt.1	$⊢ Ⅎ x φ$
2		sge0revalmpt.2	$⊢ φ \to A \in V$
3		sge0revalmpt.3	$⊢ (φ \land x \in A) \to B \in [0, +∞)$
4		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
5	1 3 4	fmptdf	$⊢ φ \to (x \in A ⟼ B) : A ⟶ [0, +∞)$
6	2 5	sge0reval	$⊢ φ \to sum^((x \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{z \in y} (x \in A ⟼ B) (z)) ℝ^{*} <)$
7		fveq2	$⊢ z = x \to (x \in A ⟼ B) (z) = (x \in A ⟼ B) (x)$
8		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
9		nfcv	$⊢ \underline{Ⅎ} x z$
10	8 9	nffv	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (z)$
11		nfcv	$⊢ \underline{Ⅎ} z (x \in A ⟼ B) (x)$
12	7 10 11	cbvsum	$⊢ \sum_{z \in y} (x \in A ⟼ B) (z) = \sum_{x \in y} (x \in A ⟼ B) (x)$
13	12	a1i	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{z \in y} (x \in A ⟼ B) (z) = \sum_{x \in y} (x \in A ⟼ B) (x)$
14		nfv	$⊢ Ⅎ x y \in (𝒫 A \cap Fin)$
15	1 14	nfan	$⊢ Ⅎ x (φ \land y \in (𝒫 A \cap Fin))$
16		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
17	16	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to y \subseteq A$
18		simpr	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in y$
19	17 18	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in A$
20	19	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to x \in A$
21		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to φ$
22	21 20 3	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to B \in [0, +∞)$
23	4	fvmpt2	$⊢ (x \in A \land B \in [0, +∞)) \to (x \in A ⟼ B) (x) = B$
24	20 22 23	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to (x \in A ⟼ B) (x) = B$
25	24	ex	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (x \in y \to (x \in A ⟼ B) (x) = B)$
26	15 25	ralrimi	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \forall x \in y (x \in A ⟼ B) (x) = B$
27		sumeq2	$⊢ \forall x \in y (x \in A ⟼ B) (x) = B \to \sum_{x \in y} (x \in A ⟼ B) (x) = \sum_{x \in y} B$
28	26 27	syl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} (x \in A ⟼ B) (x) = \sum_{x \in y} B$
29	13 28	eqtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{z \in y} (x \in A ⟼ B) (z) = \sum_{x \in y} B$
30	29	mpteq2dva	$⊢ φ \to (y \in (𝒫 A \cap Fin) ⟼ \sum_{z \in y} (x \in A ⟼ B) (z)) = (y \in (𝒫 A \cap Fin) ⟼ \sum_{x \in y} B)$
31	30	rneqd	$⊢ φ \to ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{z \in y} (x \in A ⟼ B) (z)) = ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{x \in y} B)$
32	31	supeq1d	$⊢ φ \to sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{z \in y} (x \in A ⟼ B) (z)) ℝ^{} <) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{x \in y} B) ℝ^{} <)$
33	6 32	eqtrd	$⊢ φ \to sum^((x \in A ⟼ B)) = sup (ran (y \in (𝒫 A \cap Fin) ⟼ \sum_{x \in y} B) ℝ^{*} <)$

Metamath Proof Explorer

Theorem sge0revalmpt

Proof