esumnul

Description: Extended sum over the empty set. (Contributed by Thierry Arnoux, 19-Feb-2017)

		Ref	Expression
	Assertion	esumnul	$⊢ \underset{x \in \emptyset}{\sum^{*}} A = 0$

Proof

Step	Hyp	Ref	Expression
1		nftru	$⊢ Ⅎ x ⊤$
2		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
3		0ex	$⊢ \emptyset \in V$
4	3	a1i	$⊢ ⊤ \to \emptyset \in V$
5		ral0	$⊢ \forall x \in \emptyset A \in [0, +∞]$
6	5	a1i	$⊢ ⊤ \to \forall x \in \emptyset A \in [0, +∞]$
7	6	r19.21bi	$⊢ (⊤ \land x \in \emptyset) \to A \in [0, +∞]$
8		pw0	$⊢ 𝒫 \emptyset = \{\emptyset\}$
9	8	ineq1i	$⊢ 𝒫 \emptyset \cap Fin = \{\emptyset\} \cap Fin$
10		0fin	$⊢ \emptyset \in Fin$
11		snssi	$⊢ \emptyset \in Fin \to \{\emptyset\} \subseteq Fin$
12		df-ss	$⊢ \{\emptyset\} \subseteq Fin \leftrightarrow \{\emptyset\} \cap Fin = \{\emptyset\}$
13	11 12	sylib	$⊢ \emptyset \in Fin \to \{\emptyset\} \cap Fin = \{\emptyset\}$
14	10 13	ax-mp	$⊢ \{\emptyset\} \cap Fin = \{\emptyset\}$
15	9 14	eqtri	$⊢ 𝒫 \emptyset \cap Fin = \{\emptyset\}$
16	15	eleq2i	$⊢ y \in (𝒫 \emptyset \cap Fin) \leftrightarrow y \in \{\emptyset\}$
17		velsn	$⊢ y \in \{\emptyset\} \leftrightarrow y = \emptyset$
18	16 17	sylbb	$⊢ y \in (𝒫 \emptyset \cap Fin) \to y = \emptyset$
19	18	mpteq1d	$⊢ y \in (𝒫 \emptyset \cap Fin) \to (x \in y ⟼ A) = (x \in \emptyset ⟼ A)$
20		mpt0	$⊢ (x \in \emptyset ⟼ A) = \emptyset$
21	19 20	eqtrdi	$⊢ y \in (𝒫 \emptyset \cap Fin) \to (x \in y ⟼ A) = \emptyset$
22	21	oveq2d	$⊢ y \in (𝒫 \emptyset \cap Fin) \to \underset{x \in y}{\sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]}} A = \sum_{ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]} \emptyset$
23		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
24	23	gsum0	$⊢ \sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]} \emptyset = 0$
25	22 24	eqtrdi	$⊢ y \in (𝒫 \emptyset \cap Fin) \to \underset{x \in y}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A = 0$
26	25	adantl	$⊢ (⊤ \land y \in (𝒫 \emptyset \cap Fin)) \to \underset{x \in y}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]}} A = 0$
27	1 2 4 7 26	esumval	$⊢ ⊤ \to \underset{x \in \emptyset}{\sum^{}} A = sup (ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) ℝ^{} <)$
28	27	mptru	$⊢ \underset{x \in \emptyset}{\sum^{}} A = sup (ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) ℝ^{} <)$
29		fconstmpt	$⊢ (𝒫 \emptyset \cap Fin) \times \{0\} = (y \in (𝒫 \emptyset \cap Fin) ⟼ 0)$
30	29	eqcomi	$⊢ (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = (𝒫 \emptyset \cap Fin) \times \{0\}$
31		0xr	$⊢ 0 \in ℝ^{*}$
32	31	rgenw	$⊢ \forall y \in (𝒫 \emptyset \cap Fin) 0 \in ℝ^{*}$
33		eqid	$⊢ (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = (y \in (𝒫 \emptyset \cap Fin) ⟼ 0)$
34	33	fnmpt	$⊢ \forall y \in (𝒫 \emptyset \cap Fin) 0 \in ℝ^{*} \to (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) Fn (𝒫 \emptyset \cap Fin)$
35	32 34	ax-mp	$⊢ (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) Fn (𝒫 \emptyset \cap Fin)$
36	3	snnz	$⊢ \{\emptyset\} \neq \emptyset$
37	15 36	eqnetri	$⊢ 𝒫 \emptyset \cap Fin \neq \emptyset$
38		fconst5	$⊢ ((y \in (𝒫 \emptyset \cap Fin) ⟼ 0) Fn (𝒫 \emptyset \cap Fin) \land 𝒫 \emptyset \cap Fin \neq \emptyset) \to ((y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = (𝒫 \emptyset \cap Fin) \times \{0\} \leftrightarrow ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = \{0\})$
39	35 37 38	mp2an	$⊢ (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = (𝒫 \emptyset \cap Fin) \times \{0\} \leftrightarrow ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = \{0\}$
40	30 39	mpbi	$⊢ ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) = \{0\}$
41	40	supeq1i	$⊢ sup (ran (y \in (𝒫 \emptyset \cap Fin) ⟼ 0) ℝ^{} <) = sup (\{0\} ℝ^{} <)$
42		xrltso	$⊢ < Or ℝ^{*}$
43		supsn	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{}) \to sup (\{0\} ℝ^{*} <) = 0$
44	42 31 43	mp2an	$⊢ sup (\{0\} ℝ^{*} <) = 0$
45	28 41 44	3eqtri	$⊢ \underset{x \in \emptyset}{\sum^{*}} A = 0$

Metamath Proof Explorer

Theorem esumnul

Proof