Theorem esum0

Description: Extended sum of zero. (Contributed by Thierry Arnoux, 3-Mar-2017)

	Ref	Expression
Hypothesis	esum0.k	⊢ Ⅎ 𝑘 𝐴
Assertion	esum0	⊢ ( 𝐴 ∈ 𝑉 → Σ* 𝑘 ∈ 𝐴 0 = 0 )

Proof

Step	Hyp	Ref	Expression
1		esum0.k	⊢ Ⅎ 𝑘 𝐴
2	1	nfel1	⊢ Ⅎ 𝑘 𝐴 ∈ 𝑉
3		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
4		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
5	4	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
6		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
7		cmnmnd	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd )
8	6 7	ax-mp	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd
9		vex	⊢ 𝑥 ∈ V
10		xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
11	10	gsumz	⊢ ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ Mnd ∧ 𝑥 ∈ V ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 0 ) ) = 0 )
12	8 9 11	mp2an	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 0 ) ) = 0
13	12	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ 𝑥 ↦ 0 ) ) = 0 )
14	2 1 3 5 13	esumval	⊢ ( 𝐴 ∈ 𝑉 → Σ* 𝑘 ∈ 𝐴 0 = sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) , ℝ* , < ) )
15		fconstmpt	⊢ ( ( 𝒫 𝐴 ∩ Fin ) × { 0 } ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 )
16	15	eqcomi	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = ( ( 𝒫 𝐴 ∩ Fin ) × { 0 } )
17		0xr	⊢ 0 ∈ ℝ*
18	17	rgenw	⊢ ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 0 ∈ ℝ*
19		eqid	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 )
20	19	fnmpt	⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) 0 ∈ ℝ* → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) Fn ( 𝒫 𝐴 ∩ Fin ) )
21	18 20	ax-mp	⊢ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) Fn ( 𝒫 𝐴 ∩ Fin )
22		0elpw	⊢ ∅ ∈ 𝒫 𝐴
23		0fi	⊢ ∅ ∈ Fin
24		elin	⊢ ( ∅ ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ∅ ∈ 𝒫 𝐴 ∧ ∅ ∈ Fin ) )
25	22 23 24	mpbir2an	⊢ ∅ ∈ ( 𝒫 𝐴 ∩ Fin )
26	25	ne0ii	⊢ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅
27		fconst5	⊢ ( ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) Fn ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝒫 𝐴 ∩ Fin ) ≠ ∅ ) → ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = ( ( 𝒫 𝐴 ∩ Fin ) × { 0 } ) ↔ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = { 0 } ) )
28	21 26 27	mp2an	⊢ ( ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = ( ( 𝒫 𝐴 ∩ Fin ) × { 0 } ) ↔ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = { 0 } )
29	16 28	mpbi	⊢ ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = { 0 }
30	29	a1i	⊢ ( 𝐴 ∈ 𝑉 → ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) = { 0 } )
31	30	supeq1d	⊢ ( 𝐴 ∈ 𝑉 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < ) )
32		xrltso	⊢ < Or ℝ*
33		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
34	32 17 33	mp2an	⊢ sup ( { 0 } , ℝ* , < ) = 0
35	31 34	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → sup ( ran ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ 0 ) , ℝ* , < ) = 0 )
36	14 35	eqtrd	⊢ ( 𝐴 ∈ 𝑉 → Σ* 𝑘 ∈ 𝐴 0 = 0 )