Metamath Proof Explorer


Theorem esum0

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

Ref Expression
Hypothesis esum0.k _ k A
Assertion esum0 A V * k A 0 = 0

Proof

Step Hyp Ref Expression
1 esum0.k _ k A
2 1 nfel1 k A 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 x 0 = 0
12 8 9 11 mp2an 𝑠 * 𝑠 0 +∞ k x 0 = 0
13 12 a1i A V x 𝒫 A Fin 𝑠 * 𝑠 0 +∞ k x 0 = 0
14 2 1 3 5 13 esumval A V * k A 0 = sup ran 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 Fin 0 *
19 eqid x 𝒫 A Fin 0 = x 𝒫 A Fin 0
20 19 fnmpt x 𝒫 A Fin 0 * x 𝒫 A Fin 0 Fn 𝒫 A Fin
21 18 20 ax-mp x 𝒫 A Fin 0 Fn 𝒫 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 0 Fn 𝒫 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 sup ran x 𝒫 A 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 A V sup ran x 𝒫 A Fin 0 * < = 0
36 14 35 eqtrd A V * k A 0 = 0