Metamath Proof Explorer

Theorem gsumge0cl

Description: Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses gsumge0cl.1 ⊢G=ℝ𝑠*↾𝑠0+∞
gsumge0cl.2 ⊢φ→X∈V
gsumge0cl.3 ⊢φ→F:X⟶0+∞
gsumge0cl.4 ⊢φ→finSupp0⁡F
Assertion gsumge0cl ⊢φ→∑GF∈0+∞

Proof

Step Hyp Ref Expression
1 gsumge0cl.1 ⊢G=ℝ𝑠*↾𝑠0+∞
2 gsumge0cl.2 ⊢φ→X∈V
3 gsumge0cl.3 ⊢φ→F:X⟶0+∞
4 gsumge0cl.4 ⊢φ→finSupp0⁡F
5 iccssxr ⊢0+∞⊆ℝ*
6 df-ss ⊢0+∞⊆ℝ*↔0+∞∩ℝ*=0+∞
7 5 6 mpbi ⊢0+∞∩ℝ*=0+∞
8 7 eqcomi ⊢0+∞=0+∞∩ℝ*
9 ovex ⊢0+∞∈V
10 xrsbas ⊢ℝ*=Baseℝ𝑠*
11 1 10 ressbas ⊢0+∞∈V→0+∞∩ℝ*=BaseG
12 9 11 ax-mp ⊢0+∞∩ℝ*=BaseG
13 8 12 eqtri ⊢0+∞=BaseG
14 eqid ⊢ℝ𝑠*↾𝑠ℝ*∖−∞=ℝ𝑠*↾𝑠ℝ*∖−∞
15 14 xrs1cmn ⊢ℝ𝑠*↾𝑠ℝ*∖−∞∈CMnd
16 cmnmnd ⊢ℝ𝑠*↾𝑠ℝ*∖−∞∈CMnd→ℝ𝑠*↾𝑠ℝ*∖−∞∈Mnd
17 15 16 ax-mp ⊢ℝ𝑠*↾𝑠ℝ*∖−∞∈Mnd
18 xrge0cmn ⊢ℝ𝑠*↾𝑠0+∞∈CMnd
19 1 18 eqeltri ⊢G∈CMnd
20 cmnmnd ⊢G∈CMnd→G∈Mnd
21 19 20 ax-mp ⊢G∈Mnd
22 17 21 pm3.2i ⊢ℝ𝑠*↾𝑠ℝ*∖−∞∈Mnd∧G∈Mnd
23 eliccxr ⊢x∈0+∞→x∈ℝ*
24 mnfxr ⊢−∞∈ℝ*
25 24 a1i ⊢x∈0+∞→−∞∈ℝ*
26 0xr ⊢0∈ℝ*
27 26 a1i ⊢x∈0+∞→0∈ℝ*
28 mnflt0 ⊢−∞<0
29 28 a1i ⊢x∈0+∞→−∞<0
30 pnfxr ⊢+∞∈ℝ*
31 30 a1i ⊢x∈0+∞→+∞∈ℝ*
32 id ⊢x∈0+∞→x∈0+∞
33 iccgelb ⊢0∈ℝ*∧+∞∈ℝ*∧x∈0+∞→0≤x
34 27 31 32 33 syl3anc ⊢x∈0+∞→0≤x
35 25 27 23 29 34 xrltletrd ⊢x∈0+∞→−∞<x
36 25 23 35 xrgtned ⊢x∈0+∞→x≠−∞
37 nelsn ⊢x≠−∞→¬x∈−∞
38 36 37 syl ⊢x∈0+∞→¬x∈−∞
39 23 38 eldifd ⊢x∈0+∞→x∈ℝ*∖−∞
40 39 rgen ⊢∀x∈0+∞x∈ℝ*∖−∞
41 dfss3 ⊢0+∞⊆ℝ*∖−∞↔∀x∈0+∞x∈ℝ*∖−∞
42 40 41 mpbir ⊢0+∞⊆ℝ*∖−∞
43 0e0iccpnf ⊢0∈0+∞
44 42 43 pm3.2i ⊢0+∞⊆ℝ*∖−∞∧0∈0+∞
45 difss ⊢ℝ*∖−∞⊆ℝ*
46 14 10 ressbas2 ⊢ℝ*∖−∞⊆ℝ*→ℝ*∖−∞=Baseℝ𝑠*↾𝑠ℝ*∖−∞
47 45 46 ax-mp ⊢ℝ*∖−∞=Baseℝ𝑠*↾𝑠ℝ*∖−∞
48 14 xrs10 ⊢0=0ℝ𝑠*↾𝑠ℝ*∖−∞
49 xrex ⊢ℝ*∈V
50 difexg ⊢ℝ*∈V→ℝ*∖−∞∈V
51 49 50 ax-mp ⊢ℝ*∖−∞∈V
52 44 simpli ⊢0+∞⊆ℝ*∖−∞
53 ressabs ⊢ℝ*∖−∞∈V∧0+∞⊆ℝ*∖−∞→ℝ𝑠*↾𝑠ℝ*∖−∞↾𝑠0+∞=ℝ𝑠*↾𝑠0+∞
54 51 52 53 mp2an ⊢ℝ𝑠*↾𝑠ℝ*∖−∞↾𝑠0+∞=ℝ𝑠*↾𝑠0+∞
55 1 eqcomi ⊢ℝ𝑠*↾𝑠0+∞=G
56 54 55 eqtr2i ⊢G=ℝ𝑠*↾𝑠ℝ*∖−∞↾𝑠0+∞
57 47 48 56 submnd0 ⊢ℝ𝑠*↾𝑠ℝ*∖−∞∈Mnd∧G∈Mnd∧0+∞⊆ℝ*∖−∞∧0∈0+∞→0=0G
58 22 44 57 mp2an ⊢0=0G
59 19 a1i ⊢φ→G∈CMnd
60 13 58 59 2 3 4 gsumcl ⊢φ→∑GF∈0+∞