Metamath Proof Explorer


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 0fin ∅ ∈ Fin
11 snssi ( ∅ ∈ Fin → { ∅ } ⊆ Fin )
12 df-ss ( { ∅ } ⊆ 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