esumval

Description: Develop the value of the extended sum. (Contributed by Thierry Arnoux, 4-Jan-2017)

	Ref	Expression
Hypotheses	esumval.p	$⊢ Ⅎ k φ$
	esumval.0	$⊢ \underline{Ⅎ} k A$
	esumval.1	$⊢ φ \to A \in V$
	esumval.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumval.3	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B = C$
Assertion	esumval	$⊢ φ \to \underset{k \in A}{\sum^{}} B = sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)$

Proof

Step	Hyp	Ref	Expression
1		esumval.p	$⊢ Ⅎ k φ$
2		esumval.0	$⊢ \underline{Ⅎ} k A$
3		esumval.1	$⊢ φ \to A \in V$
4		esumval.2	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
5		esumval.3	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \underset{k \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} B = C$
6		df-esum	$⊢ \underset{k \in A}{\sum^{}} B = ⋃ ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B))$
7		eqid	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]$
8		nfcv	$⊢ \underline{Ⅎ} k [0, +∞]$
9		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
10	1 2 8 4 9	fmptdF	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
11		inss1	$⊢ 𝒫 A \cap Fin \subseteq 𝒫 A$
12	11	sseli	$⊢ x \in (𝒫 A \cap Fin) \to x \in 𝒫 A$
13	12	elpwid	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
14	13	adantl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to x \subseteq A$
15		nfcv	$⊢ \underline{Ⅎ} k x$
16	2 15	resmptf	$⊢ x \subseteq A \to {(k \in A ⟼ B) ↾}_{x} = (k \in x ⟼ B)$
17	14 16	syl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to {(k \in A ⟼ B) ↾}_{x} = (k \in x ⟼ B)$
18	17	oveq2d	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{x}) = \underset{k \in x}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} B$
19	18 5	eqtr2d	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to C = \sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{x})$
20	19	mpteq2dva	$⊢ φ \to (x \in (𝒫 A \cap Fin) ⟼ C) = (x \in (𝒫 A \cap Fin) ⟼ \sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{x}))$
21	20	rneqd	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ C) = ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{x}))$
22	21	supeq1d	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} ({(k \in A ⟼ B) ↾}_{x})) ℝ^{*} <)$
23	7 3 10 22	xrge0tsmsd	$⊢ φ \to (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B) = \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)\}$
24	23	unieqd	$⊢ φ \to ⋃ ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B)) = ⋃ \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)\}$
25	6 24	eqtrid	$⊢ φ \to \underset{k \in A}{\sum^{}} B = ⋃ \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)\}$
26		xrltso	$⊢ < Or ℝ^{*}$
27	26	supex	$⊢ sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{*} <) \in V$
28	27	unisn	$⊢ ⋃ \{sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)\} = sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)$
29	25 28	eqtrdi	$⊢ φ \to \underset{k \in A}{\sum^{}} B = sup (ran (x \in (𝒫 A \cap Fin) ⟼ C) ℝ^{} <)$

Metamath Proof Explorer

Theorem esumval

Proof