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		nfcv	$⊢ \underline{Ⅎ} x y$
9		nfcv	$⊢ \underline{Ⅎ} z y$
10		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
11		nfcv	$⊢ \underline{Ⅎ} x z$
12	10 11	nffv	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (z)$
13		nfcv	$⊢ \underline{Ⅎ} z (x \in A ⟼ B) (x)$
14	7 8 9 12 13	cbvsum	$⊢ \sum_{z \in y} (x \in A ⟼ B) (z) = \sum_{x \in y} (x \in A ⟼ B) (x)$
15	14	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)$
16		nfv	$⊢ Ⅎ x y \in (𝒫 A \cap Fin)$
17	1 16	nfan	$⊢ Ⅎ x (φ \land y \in (𝒫 A \cap Fin))$
18		elpwinss	$⊢ y \in (𝒫 A \cap Fin) \to y \subseteq A$
19	18	adantr	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to y \subseteq A$
20		simpr	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in y$
21	19 20	sseldd	$⊢ (y \in (𝒫 A \cap Fin) \land x \in y) \to x \in A$
22	21	adantll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to x \in A$
23		simpll	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to φ$
24	23 22 3	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to B \in [0, +∞)$
25	4	fvmpt2	$⊢ (x \in A \land B \in [0, +∞)) \to (x \in A ⟼ B) (x) = B$
26	22 24 25	syl2anc	$⊢ ((φ \land y \in (𝒫 A \cap Fin)) \land x \in y) \to (x \in A ⟼ B) (x) = B$
27	26	ex	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to (x \in y \to (x \in A ⟼ B) (x) = B)$
28	17 27	ralrimi	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \forall x \in y (x \in A ⟼ B) (x) = B$
29		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$
30	28 29	syl	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{x \in y} (x \in A ⟼ B) (x) = \sum_{x \in y} B$
31	15 30	eqtrd	$⊢ (φ \land y \in (𝒫 A \cap Fin)) \to \sum_{z \in y} (x \in A ⟼ B) (z) = \sum_{x \in y} B$
32	31	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)$
33	32	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)$
34	33	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) ℝ^{} <)$
35	6 34	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