sge0z

Description: Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0z.1	$⊢ Ⅎ k φ$
	sge0z.2	$⊢ φ \to A \in V$
Assertion	sge0z	$⊢ φ \to sum^((k \in A ⟼ 0)) = 0$

Proof

Step	Hyp	Ref	Expression
1		sge0z.1	$⊢ Ⅎ k φ$
2		sge0z.2	$⊢ φ \to A \in V$
3		0e0icopnf	$⊢ 0 \in [0, +∞)$
4	3	a1i	$⊢ (φ \land k \in A) \to 0 \in [0, +∞)$
5	1 4	fmptd2f	$⊢ φ \to (k \in A ⟼ 0) : A ⟶ [0, +∞)$
6	2 5	sge0reval	$⊢ φ \to sum^((k \in A ⟼ 0)) = sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} (k \in A ⟼ 0) (y)) ℝ^{*} <)$
7		eqidd	$⊢ (x \in (𝒫 A \cap Fin) \land y \in x) \to (k \in A ⟼ 0) = (k \in A ⟼ 0)$
8		eqidd	$⊢ ((x \in (𝒫 A \cap Fin) \land y \in x) \land k = y) \to 0 = 0$
9		elpwinss	$⊢ x \in (𝒫 A \cap Fin) \to x \subseteq A$
10	9	sselda	$⊢ (x \in (𝒫 A \cap Fin) \land y \in x) \to y \in A$
11		0cnd	$⊢ (x \in (𝒫 A \cap Fin) \land y \in x) \to 0 \in ℂ$
12	7 8 10 11	fvmptd	$⊢ (x \in (𝒫 A \cap Fin) \land y \in x) \to (k \in A ⟼ 0) (y) = 0$
13	12	adantll	$⊢ ((φ \land x \in (𝒫 A \cap Fin)) \land y \in x) \to (k \in A ⟼ 0) (y) = 0$
14	13	sumeq2dv	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{y \in x} (k \in A ⟼ 0) (y) = \sum_{y \in x} 0$
15		elinel2	$⊢ x \in (𝒫 A \cap Fin) \to x \in Fin$
16		olc	$⊢ x \in Fin \to (x \subseteq ℤ_{\geq B} \lor x \in Fin)$
17		sumz	$⊢ (x \subseteq ℤ_{\geq B} \lor x \in Fin) \to \sum_{y \in x} 0 = 0$
18	15 16 17	3syl	$⊢ x \in (𝒫 A \cap Fin) \to \sum_{y \in x} 0 = 0$
19	18	adantl	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{y \in x} 0 = 0$
20	14 19	eqtrd	$⊢ (φ \land x \in (𝒫 A \cap Fin)) \to \sum_{y \in x} (k \in A ⟼ 0) (y) = 0$
21	20	mpteq2dva	$⊢ φ \to (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} (k \in A ⟼ 0) (y)) = (x \in (𝒫 A \cap Fin) ⟼ 0)$
22	21	rneqd	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} (k \in A ⟼ 0) (y)) = ran (x \in (𝒫 A \cap Fin) ⟼ 0)$
23		eqid	$⊢ (x \in (𝒫 A \cap Fin) ⟼ 0) = (x \in (𝒫 A \cap Fin) ⟼ 0)$
24		pwfin0	$⊢ 𝒫 A \cap Fin \neq \emptyset$
25	24	a1i	$⊢ φ \to 𝒫 A \cap Fin \neq \emptyset$
26	23 25	rnmptc	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ 0) = \{0\}$
27	22 26	eqtrd	$⊢ φ \to ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} (k \in A ⟼ 0) (y)) = \{0\}$
28	27	supeq1d	$⊢ φ \to sup (ran (x \in (𝒫 A \cap Fin) ⟼ \sum_{y \in x} (k \in A ⟼ 0) (y)) ℝ^{} <) = sup (\{0\} ℝ^{} <)$
29		xrltso	$⊢ < Or ℝ^{*}$
30	29	a1i	$⊢ φ \to < Or ℝ^{*}$
31		0xr	$⊢ 0 \in ℝ^{*}$
32		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
33	30 31 32	sylancl	$⊢ φ \to sup (\{0\} ℝ^{*} <) = 0$
34	6 28 33	3eqtrd	$⊢ φ \to sum^((k \in A ⟼ 0)) = 0$

Metamath Proof Explorer

Theorem sge0z

Proof