sge0sn

Description: A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0sn.1	$⊢ φ \to A \in V$
	sge0sn.2	$⊢ φ \to F : \{A\} ⟶ [0, +∞]$
Assertion	sge0sn	$⊢ φ \to sum^(F) = F (A)$

Proof

Step	Hyp	Ref	Expression
1		sge0sn.1	$⊢ φ \to A \in V$
2		sge0sn.2	$⊢ φ \to F : \{A\} ⟶ [0, +∞]$
3		snex	$⊢ \{A\} \in V$
4	3	a1i	$⊢ (φ \land F (A) = +∞) \to \{A\} \in V$
5	2	adantr	$⊢ (φ \land F (A) = +∞) \to F : \{A\} ⟶ [0, +∞]$
6		id	$⊢ F (A) = +∞ \to F (A) = +∞$
7	6	eqcomd	$⊢ F (A) = +∞ \to +∞ = F (A)$
8	7	adantl	$⊢ (φ \land F (A) = +∞) \to +∞ = F (A)$
9	2	ffund	$⊢ φ \to Fun F$
10	9	adantr	$⊢ (φ \land F (A) = +∞) \to Fun F$
11		snidg	$⊢ A \in V \to A \in \{A\}$
12	1 11	syl	$⊢ φ \to A \in \{A\}$
13	2	fdmd	$⊢ φ \to dom F = \{A\}$
14	13	eqcomd	$⊢ φ \to \{A\} = dom F$
15	12 14	eleqtrd	$⊢ φ \to A \in dom F$
16	15	adantr	$⊢ (φ \land F (A) = +∞) \to A \in dom F$
17		fvelrn	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$
18	10 16 17	syl2anc	$⊢ (φ \land F (A) = +∞) \to F (A) \in ran F$
19	8 18	eqeltrd	$⊢ (φ \land F (A) = +∞) \to +∞ \in ran F$
20	4 5 19	sge0pnfval	$⊢ (φ \land F (A) = +∞) \to sum^(F) = +∞$
21		simpr	$⊢ (φ \land F (A) = +∞) \to F (A) = +∞$
22	20 21	eqtr4d	$⊢ (φ \land F (A) = +∞) \to sum^(F) = F (A)$
23	3	a1i	$⊢ (φ \land \neg F (A) = +∞) \to \{A\} \in V$
24	2	adantr	$⊢ (φ \land \neg F (A) = +∞) \to F : \{A\} ⟶ [0, +∞]$
25		elsni	$⊢ +∞ \in \{F (A)\} \to +∞ = F (A)$
26	25	eqcomd	$⊢ +∞ \in \{F (A)\} \to F (A) = +∞$
27	26	con3i	$⊢ \neg F (A) = +∞ \to \neg +∞ \in \{F (A)\}$
28	27	adantl	$⊢ (φ \land \neg F (A) = +∞) \to \neg +∞ \in \{F (A)\}$
29	1 2	rnsnf	$⊢ φ \to ran F = \{F (A)\}$
30	29	eqcomd	$⊢ φ \to \{F (A)\} = ran F$
31	30	adantr	$⊢ (φ \land \neg F (A) = +∞) \to \{F (A)\} = ran F$
32	28 31	neleqtrd	$⊢ (φ \land \neg F (A) = +∞) \to \neg +∞ \in ran F$
33	24 32	fge0iccico	$⊢ (φ \land \neg F (A) = +∞) \to F : \{A\} ⟶ [0, +∞)$
34	23 33	sge0reval	$⊢ (φ \land \neg F (A) = +∞) \to sum^(F) = sup (ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
35		sum0	$⊢ \sum_{y \in \emptyset} F (y) = 0$
36	35	eqcomi	$⊢ 0 = \sum_{y \in \emptyset} F (y)$
37	36	a1i	$⊢ (φ \land \neg F (A) = +∞) \to 0 = \sum_{y \in \emptyset} F (y)$
38		nfcvd	$⊢ (φ \land \neg F (A) = +∞) \to \underline{Ⅎ} y F (A)$
39		nfv	$⊢ Ⅎ y (φ \land \neg F (A) = +∞)$
40		fveq2	$⊢ y = A \to F (y) = F (A)$
41	40	adantl	$⊢ ((φ \land \neg F (A) = +∞) \land y = A) \to F (y) = F (A)$
42	1	adantr	$⊢ (φ \land \neg F (A) = +∞) \to A \in V$
43		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
44		ax-resscn	$⊢ ℝ \subseteq ℂ$
45	43 44	sstri	$⊢ [0, +∞) \subseteq ℂ$
46	42 11	syl	$⊢ (φ \land \neg F (A) = +∞) \to A \in \{A\}$
47	33 46	ffvelrnd	$⊢ (φ \land \neg F (A) = +∞) \to F (A) \in [0, +∞)$
48	45 47	sselid	$⊢ (φ \land \neg F (A) = +∞) \to F (A) \in ℂ$
49	38 39 41 42 48	sumsnd	$⊢ (φ \land \neg F (A) = +∞) \to \sum_{y \in \{A\}} F (y) = F (A)$
50	49	eqcomd	$⊢ (φ \land \neg F (A) = +∞) \to F (A) = \sum_{y \in \{A\}} F (y)$
51	37 50	preq12d	$⊢ (φ \land \neg F (A) = +∞) \to \{0, F (A)\} = \{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\}$
52	51	supeq1d	$⊢ (φ \land \neg F (A) = +∞) \to sup (\{0, F (A)\} ℝ^{} <) = sup (\{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\} ℝ^{} <)$
53		xrltso	$⊢ < Or ℝ^{*}$
54	53	a1i	$⊢ φ \to < Or ℝ^{*}$
55		0xr	$⊢ 0 \in ℝ^{*}$
56	55	a1i	$⊢ φ \to 0 \in ℝ^{*}$
57		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
58	2 12	ffvelrnd	$⊢ φ \to F (A) \in [0, +∞]$
59	57 58	sselid	$⊢ φ \to F (A) \in ℝ^{*}$
60		suppr	$⊢ (< Or ℝ^{} \land 0 \in ℝ^{} \land F (A) \in ℝ^{}) \to sup (\{0, F (A)\} ℝ^{} <) = if (F (A) < 0, 0, F (A))$
61	54 56 59 60	syl3anc	$⊢ φ \to sup (\{0, F (A)\} ℝ^{*} <) = if (F (A) < 0, 0, F (A))$
62		pnfxr	$⊢ +∞ \in ℝ^{*}$
63	62	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
64	56 63 58	3jca	$⊢ φ \to (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (A) \in [0, +∞])$
65		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (A) \in [0, +∞]) \to 0 \leq F (A)$
66	64 65	syl	$⊢ φ \to 0 \leq F (A)$
67	56 59	xrlenltd	$⊢ φ \to (0 \leq F (A) \leftrightarrow \neg F (A) < 0)$
68	66 67	mpbid	$⊢ φ \to \neg F (A) < 0$
69	68	iffalsed	$⊢ φ \to if (F (A) < 0, 0, F (A)) = F (A)$
70	61 69	eqtr2d	$⊢ φ \to F (A) = sup (\{0, F (A)\} ℝ^{*} <)$
71	70	adantr	$⊢ (φ \land \neg F (A) = +∞) \to F (A) = sup (\{0, F (A)\} ℝ^{*} <)$
72		pwsn	$⊢ 𝒫 \{A\} = \{\emptyset, \{A\}\}$
73	72	ineq1i	$⊢ 𝒫 \{A\} \cap Fin = \{\emptyset, \{A\}\} \cap Fin$
74		0fin	$⊢ \emptyset \in Fin$
75		snfi	$⊢ \{A\} \in Fin$
76		prssi	$⊢ (\emptyset \in Fin \land \{A\} \in Fin) \to \{\emptyset, \{A\}\} \subseteq Fin$
77	74 75 76	mp2an	$⊢ \{\emptyset, \{A\}\} \subseteq Fin$
78		df-ss	$⊢ \{\emptyset, \{A\}\} \subseteq Fin \leftrightarrow \{\emptyset, \{A\}\} \cap Fin = \{\emptyset, \{A\}\}$
79	78	biimpi	$⊢ \{\emptyset, \{A\}\} \subseteq Fin \to \{\emptyset, \{A\}\} \cap Fin = \{\emptyset, \{A\}\}$
80	77 79	ax-mp	$⊢ \{\emptyset, \{A\}\} \cap Fin = \{\emptyset, \{A\}\}$
81	73 80	eqtri	$⊢ 𝒫 \{A\} \cap Fin = \{\emptyset, \{A\}\}$
82		mpteq1	$⊢ 𝒫 \{A\} \cap Fin = \{\emptyset, \{A\}\} \to (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in \{\emptyset, \{A\}\} ⟼ \sum_{y \in x} F (y))$
83	81 82	ax-mp	$⊢ (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in \{\emptyset, \{A\}\} ⟼ \sum_{y \in x} F (y))$
84		0ex	$⊢ \emptyset \in V$
85	84	a1i	$⊢ ⊤ \to \emptyset \in V$
86	3	a1i	$⊢ ⊤ \to \{A\} \in V$
87		sumex	$⊢ \sum_{y \in \emptyset} F (y) \in V$
88	87	a1i	$⊢ ⊤ \to \sum_{y \in \emptyset} F (y) \in V$
89		sumex	$⊢ \sum_{y \in \{A\}} F (y) \in V$
90	89	a1i	$⊢ ⊤ \to \sum_{y \in \{A\}} F (y) \in V$
91		sumeq1	$⊢ x = \emptyset \to \sum_{y \in x} F (y) = \sum_{y \in \emptyset} F (y)$
92	91	adantl	$⊢ (⊤ \land x = \emptyset) \to \sum_{y \in x} F (y) = \sum_{y \in \emptyset} F (y)$
93		sumeq1	$⊢ x = \{A\} \to \sum_{y \in x} F (y) = \sum_{y \in \{A\}} F (y)$
94	93	adantl	$⊢ (⊤ \land x = \{A\}) \to \sum_{y \in x} F (y) = \sum_{y \in \{A\}} F (y)$
95	85 86 88 90 92 94	fmptpr	$⊢ ⊤ \to \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\} = (x \in \{\emptyset, \{A\}\} ⟼ \sum_{y \in x} F (y))$
96	95	mptru	$⊢ \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\} = (x \in \{\emptyset, \{A\}\} ⟼ \sum_{y \in x} F (y))$
97	96	eqcomi	$⊢ (x \in \{\emptyset, \{A\}\} ⟼ \sum_{y \in x} F (y)) = \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\}$
98	83 97	eqtri	$⊢ (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) = \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\}$
99	98	rneqi	$⊢ ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) = ran \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\}$
100		rnpropg	$⊢ (\emptyset \in V \land \{A\} \in V) \to ran \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\} = \{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\}$
101	84 3 100	mp2an	$⊢ ran \{⟨\emptyset, \sum_{y \in \emptyset} F (y)⟩, ⟨\{A\}, \sum_{y \in \{A\}} F (y)⟩\} = \{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\}$
102	99 101	eqtri	$⊢ ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) = \{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\}$
103	102	supeq1i	$⊢ sup (ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) = sup (\{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\} ℝ^{} <)$
104	103	a1i	$⊢ (φ \land \neg F (A) = +∞) \to sup (ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) = sup (\{\sum_{y \in \emptyset} F (y), \sum_{y \in \{A\}} F (y)\} ℝ^{} <)$
105	52 71 104	3eqtr4d	$⊢ (φ \land \neg F (A) = +∞) \to F (A) = sup (ran (x \in (𝒫 \{A\} \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
106	34 105	eqtr4d	$⊢ (φ \land \neg F (A) = +∞) \to sum^(F) = F (A)$
107	22 106	pm2.61dan	$⊢ φ \to sum^(F) = F (A)$

Metamath Proof Explorer

Theorem sge0sn

Proof