Theorem sge00

Description: The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	sge00	⊢ ( Σ^ ‘ ∅ ) = 0

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2	1	a1i	⊢ ( ⊤ → ∅ ∈ V )
3		f0	⊢ ∅ : ∅ ⟶ ( 0 [,] +∞ )
4	3	a1i	⊢ ( ⊤ → ∅ : ∅ ⟶ ( 0 [,] +∞ ) )
5		noel	⊢ ¬ +∞ ∈ ∅
6	5	a1i	⊢ ( ⊤ → ¬ +∞ ∈ ∅ )
7		rn0	⊢ ran ∅ = ∅
8	7	eqcomi	⊢ ∅ = ran ∅
9	8	a1i	⊢ ( ⊤ → ∅ = ran ∅ )
10	6 9	neleqtrd	⊢ ( ⊤ → ¬ +∞ ∈ ran ∅ )
11	4 10	fge0iccico	⊢ ( ⊤ → ∅ : ∅ ⟶ ( 0 [,) +∞ ) )
12	2 11	sge0reval	⊢ ( ⊤ → ( Σ^ ‘ ∅ ) = sup ( ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) , ℝ* , < ) )
13	12	mptru	⊢ ( Σ^ ‘ ∅ ) = sup ( ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) , ℝ* , < )
14		vex	⊢ 𝑧 ∈ V
15		eqid	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) = ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
16	15	elrnmpt	⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) )
17	14 16	ax-mp	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
18	17	biimpi	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
19		nfcv	⊢ Ⅎ 𝑥 𝑧
20		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
21	20	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
22	19 21	nfel	⊢ Ⅎ 𝑥 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
23		nfv	⊢ Ⅎ 𝑥 𝑧 = 0
24		simpr	⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
25		elinel1	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 ∈ 𝒫 ∅ )
26		pw0	⊢ 𝒫 ∅ = { ∅ }
27	26	eleq2i	⊢ ( 𝑥 ∈ 𝒫 ∅ ↔ 𝑥 ∈ { ∅ } )
28	27	biimpi	⊢ ( 𝑥 ∈ 𝒫 ∅ → 𝑥 ∈ { ∅ } )
29	25 28	syl	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 ∈ { ∅ } )
30		elsni	⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
31	29 30	syl	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = ∅ )
32	31	sumeq1d	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) )
33	32	adantr	⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) )
34		sum0	⊢ Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) = 0
35	34	a1i	⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) = 0 )
36	24 33 35	3eqtrd	⊢ ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → 𝑧 = 0 )
37	36	ex	⊢ ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) → 𝑧 = 0 ) )
38	37	a1i	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) → 𝑧 = 0 ) ) )
39	22 23 38	rexlimd	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑧 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) → 𝑧 = 0 ) )
40	18 39	mpd	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → 𝑧 = 0 )
41		velsn	⊢ ( 𝑧 ∈ { 0 } ↔ 𝑧 = 0 )
42	41	bicomi	⊢ ( 𝑧 = 0 ↔ 𝑧 ∈ { 0 } )
43	42	biimpi	⊢ ( 𝑧 = 0 → 𝑧 ∈ { 0 } )
44	40 43	syl	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) → 𝑧 ∈ { 0 } )
45		elsni	⊢ ( 𝑧 ∈ { 0 } → 𝑧 = 0 )
46		0elpw	⊢ ∅ ∈ 𝒫 ∅
47		0fi	⊢ ∅ ∈ Fin
48	46 47	pm3.2i	⊢ ( ∅ ∈ 𝒫 ∅ ∧ ∅ ∈ Fin )
49		elin	⊢ ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ↔ ( ∅ ∈ 𝒫 ∅ ∧ ∅ ∈ Fin ) )
50	48 49	mpbir	⊢ ∅ ∈ ( 𝒫 ∅ ∩ Fin )
51	34	eqcomi	⊢ 0 = Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 )
52		sumeq1	⊢ ( 𝑥 = ∅ → Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) = Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) )
53	52	rspceeqv	⊢ ( ( ∅ ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 0 = Σ 𝑦 ∈ ∅ ( ∅ ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
54	50 51 53	mp2an	⊢ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 )
55		0re	⊢ 0 ∈ ℝ
56	15	elrnmpt	⊢ ( 0 ∈ ℝ → ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) )
57	55 56	ax-mp	⊢ ( 0 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 0 = Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
58	54 57	mpbir	⊢ 0 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) )
59	58	a1i	⊢ ( 𝑧 ∈ { 0 } → 0 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) )
60	45 59	eqeltrd	⊢ ( 𝑧 ∈ { 0 } → 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) )
61	44 60	impbii	⊢ ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ 𝑧 ∈ { 0 } )
62	61	ax-gen	⊢ ∀ 𝑧 ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ 𝑧 ∈ { 0 } )
63		dfcleq	⊢ ( ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) = { 0 } ↔ ∀ 𝑧 ( 𝑧 ∈ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) ↔ 𝑧 ∈ { 0 } ) )
64	62 63	mpbir	⊢ ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) = { 0 }
65	64	supeq1i	⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
66		xrltso	⊢ < Or ℝ*
67		0xr	⊢ 0 ∈ ℝ*
68		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
69	66 67 68	mp2an	⊢ sup ( { 0 } , ℝ* , < ) = 0
70	65 69	eqtri	⊢ sup ( ran ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( ∅ ‘ 𝑦 ) ) , ℝ* , < ) = 0
71	13 70	eqtri	⊢ ( Σ^ ‘ ∅ ) = 0