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 ⊢ φ → finSupp 0 ⁡ F
Assertion gsumge0cl ⊢ φ → ∑ G F ∈ 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 ⊢ φ → finSupp 0 ⁡ 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 +∞ ∩ ℝ * = Base G
12 9 11 ax-mp ⊢ 0 +∞ ∩ ℝ * = Base G
13 8 12 eqtri ⊢ 0 +∞ = Base G
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 = 0 G
58 22 44 57 mp2an ⊢ 0 = 0 G
59 19 a1i ⊢ φ → G ∈ CMnd
60 13 58 59 2 3 4 gsumcl ⊢ φ → ∑ G F ∈ 0 +∞