Theorem esumnul

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

	Ref	Expression
Assertion	esumnul	⊢ Σ* 𝑥 ∈ ∅ 𝐴 = 0

Proof

Step	Hyp	Ref	Expression
1		nftru	⊢ Ⅎ 𝑥 ⊤
2		nfcv	⊢ Ⅎ 𝑥 ∅
3		0ex	⊢ ∅ ∈ V
4	3	a1i	⊢ ( ⊤ → ∅ ∈ V )
5		ral0	⊢ ∀ 𝑥 ∈ ∅ 𝐴 ∈ ( 0 [,] +∞ )
6	5	a1i	⊢ ( ⊤ → ∀ 𝑥 ∈ ∅ 𝐴 ∈ ( 0 [,] +∞ ) )
7	6	r19.21bi	⊢ ( ( ⊤ ∧ 𝑥 ∈ ∅ ) → 𝐴 ∈ ( 0 [,] +∞ ) )
8		pw0	⊢ 𝒫 ∅ = { ∅ }
9	8	ineq1i	⊢ ( 𝒫 ∅ ∩ Fin ) = ( { ∅ } ∩ Fin )
10		0fi	⊢ ∅ ∈ Fin
11		snssi	⊢ ( ∅ ∈ Fin → { ∅ } ⊆ Fin )
12		dfss2	⊢ ( { ∅ } ⊆ Fin ↔ ( { ∅ } ∩ Fin ) = { ∅ } )
13	11 12	sylib	⊢ ( ∅ ∈ Fin → ( { ∅ } ∩ Fin ) = { ∅ } )
14	10 13	ax-mp	⊢ ( { ∅ } ∩ Fin ) = { ∅ }
15	9 14	eqtri	⊢ ( 𝒫 ∅ ∩ Fin ) = { ∅ }
16	15	eleq2i	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↔ 𝑦 ∈ { ∅ } )
17		velsn	⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
18	16 17	sylbb	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑦 = ∅ )
19	18	mpteq1d	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) = ( 𝑥 ∈ ∅ ↦ 𝐴 ) )
20		mpt0	⊢ ( 𝑥 ∈ ∅ ↦ 𝐴 ) = ∅
21	19 20	eqtrdi	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) = ∅ )
22	21	oveq2d	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) )
23		xrge00	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
24	23	gsum0	⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ∅ ) = 0
25	22 24	eqtrdi	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = 0 )
26	25	adantl	⊢ ( ( ⊤ ∧ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑥 ∈ 𝑦 ↦ 𝐴 ) ) = 0 )
27	1 2 4 7 26	esumval	⊢ ( ⊤ → Σ* 𝑥 ∈ ∅ 𝐴 = sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < ) )
28	27	mptru	⊢ Σ* 𝑥 ∈ ∅ 𝐴 = sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < )
29		fconstmpt	⊢ ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) = ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 )
30	29	eqcomi	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } )
31		0xr	⊢ 0 ∈ ℝ*
32	31	rgenw	⊢ ∀ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) 0 ∈ ℝ*
33		eqid	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 )
34	33	fnmpt	⊢ ( ∀ 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) 0 ∈ ℝ* → ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin ) )
35	32 34	ax-mp	⊢ ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin )
36	3	snnz	⊢ { ∅ } ≠ ∅
37	15 36	eqnetri	⊢ ( 𝒫 ∅ ∩ Fin ) ≠ ∅
38		fconst5	⊢ ( ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) Fn ( 𝒫 ∅ ∩ Fin ) ∧ ( 𝒫 ∅ ∩ Fin ) ≠ ∅ ) → ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) ↔ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 } ) )
39	35 37 38	mp2an	⊢ ( ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = ( ( 𝒫 ∅ ∩ Fin ) × { 0 } ) ↔ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 } )
40	30 39	mpbi	⊢ ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) = { 0 }
41	40	supeq1i	⊢ sup ( ran ( 𝑦 ∈ ( 𝒫 ∅ ∩ Fin ) ↦ 0 ) , ℝ* , < ) = sup ( { 0 } , ℝ* , < )
42		xrltso	⊢ < Or ℝ*
43		supsn	⊢ ( ( < Or ℝ* ∧ 0 ∈ ℝ* ) → sup ( { 0 } , ℝ* , < ) = 0 )
44	42 31 43	mp2an	⊢ sup ( { 0 } , ℝ* , < ) = 0
45	28 41 44	3eqtri	⊢ Σ* 𝑥 ∈ ∅ 𝐴 = 0