Metamath Proof Explorer

Theorem esum0

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

Ref Expression
Hypothesis esum0.k ⊢Ⅎ_kA
Assertion esum0 ⊢A∈V→∑*k∈A0=0

Proof

Step Hyp Ref Expression
1 esum0.k ⊢Ⅎ_kA
2 1 nfel1 ⊢ℲkA∈V
3 id ⊢A∈V→A∈V
4 0e0iccpnf ⊢0∈0+∞
5 4 a1i ⊢A∈V∧k∈A→0∈0+∞
6 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
7 cmnmnd ⊢ℝ𝑠*↾𝑠0+∞∈CMnd→ℝ𝑠*↾𝑠0+∞∈Mnd
8 6 7 ax-mp ⊢ℝ𝑠*↾𝑠0+∞∈Mnd
9 vex ⊢x∈V
10 xrge00 ⊢0=0ℝ𝑠*↾𝑠0+∞
11 10 gsumz ⊢ℝ𝑠*↾𝑠0+∞∈Mnd∧x∈V→∑ℝ𝑠*↾𝑠0+∞k∈x0=0
12 8 9 11 mp2an ⊢∑ℝ𝑠*↾𝑠0+∞k∈x0=0
13 12 a1i ⊢A∈V∧x∈𝒫A∩Fin→∑ℝ𝑠*↾𝑠0+∞k∈x0=0
14 2 1 3 5 13 esumval ⊢A∈V→∑*k∈A0=supran⁡x∈𝒫A∩Fin⟼0ℝ*<
15 fconstmpt ⊢𝒫A∩Fin×0=x∈𝒫A∩Fin⟼0
16 15 eqcomi ⊢x∈𝒫A∩Fin⟼0=𝒫A∩Fin×0
17 0xr ⊢0∈ℝ*
18 17 rgenw ⊢∀x∈𝒫A∩Fin0∈ℝ*
19 eqid ⊢x∈𝒫A∩Fin⟼0=x∈𝒫A∩Fin⟼0
20 19 fnmpt ⊢∀x∈𝒫A∩Fin0∈ℝ*→x∈𝒫A∩Fin⟼0Fn𝒫A∩Fin
21 18 20 ax-mp ⊢x∈𝒫A∩Fin⟼0Fn𝒫A∩Fin
22 0elpw ⊢∅∈𝒫A
23 0fin ⊢∅∈Fin
24 elin ⊢∅∈𝒫A∩Fin↔∅∈𝒫A∧∅∈Fin
25 22 23 24 mpbir2an ⊢∅∈𝒫A∩Fin
26 25 ne0ii ⊢𝒫A∩Fin≠∅
27 fconst5 ⊢x∈𝒫A∩Fin⟼0Fn𝒫A∩Fin∧𝒫A∩Fin≠∅→x∈𝒫A∩Fin⟼0=𝒫A∩Fin×0↔ran⁡x∈𝒫A∩Fin⟼0=0
28 21 26 27 mp2an ⊢x∈𝒫A∩Fin⟼0=𝒫A∩Fin×0↔ran⁡x∈𝒫A∩Fin⟼0=0
29 16 28 mpbi ⊢ran⁡x∈𝒫A∩Fin⟼0=0
30 29 a1i ⊢A∈V→ran⁡x∈𝒫A∩Fin⟼0=0
31 30 supeq1d ⊢A∈V→supran⁡x∈𝒫A∩Fin⟼0ℝ*<=sup0ℝ*<
32 xrltso ⊢<Orℝ*
33 supsn ⊢<Orℝ*∧0∈ℝ*→sup0ℝ*<=0
34 32 17 33 mp2an ⊢sup0ℝ*<=0
35 31 34 eqtrdi ⊢A∈V→supran⁡x∈𝒫A∩Fin⟼0ℝ*<=0
36 14 35 eqtrd ⊢A∈V→∑*k∈A0=0