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	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
	gsumge0cl.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	gsumge0cl.3	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	gsumge0cl.4	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	gsumge0cl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		gsumge0cl.1	⊢ 𝐺 = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
2		gsumge0cl.2	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
3		gsumge0cl.3	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
4		gsumge0cl.4	⊢ ( 𝜑 → 𝐹 finSupp 0 )
5		iccssxr	⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6		dfss2	⊢ ( ( 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 ‘ 𝐺 ) )
12	9 11	ax-mp	⊢ ( ( 0 [,] +∞ ) ∩ ℝ* ) = ( Base ‘ 𝐺 )
13	8 12	eqtri	⊢ ( 0 [,] +∞ ) = ( Base ‘ 𝐺 )
14		eqid	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
15	14	xrs1cmn	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd
16		cmnmnd	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ CMnd → ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd )
17	15 16	ax-mp	⊢ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd
18		xrge0cmn	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
19	1 18	eqeltri	⊢ 𝐺 ∈ CMnd
20		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
21	19 20	ax-mp	⊢ 𝐺 ∈ Mnd
22	17 21	pm3.2i	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd ∧ 𝐺 ∈ Mnd )
23		eliccxr	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ℝ* )
24		mnfxr	⊢ -∞ ∈ ℝ*
25	24	a1i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → -∞ ∈ ℝ* )
26		0xr	⊢ 0 ∈ ℝ*
27	26	a1i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 0 ∈ ℝ* )
28		mnflt0	⊢ -∞ < 0
29	28	a1i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → -∞ < 0 )
30		pnfxr	⊢ +∞ ∈ ℝ*
31	30	a1i	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → +∞ ∈ ℝ* )
32		id	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ( 0 [,] +∞ ) )
33		iccgelb	⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → 0 ≤ 𝑥 )
34	27 31 32 33	syl3anc	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 0 ≤ 𝑥 )
35	25 27 23 29 34	xrltletrd	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → -∞ < 𝑥 )
36	25 23 35	xrgtned	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ≠ -∞ )
37		nelsn	⊢ ( 𝑥 ≠ -∞ → ¬ 𝑥 ∈ { -∞ } )
38	36 37	syl	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → ¬ 𝑥 ∈ { -∞ } )
39	23 38	eldifd	⊢ ( 𝑥 ∈ ( 0 [,] +∞ ) → 𝑥 ∈ ( ℝ* ∖ { -∞ } ) )
40	39	rgen	⊢ ∀ 𝑥 ∈ ( 0 [,] +∞ ) 𝑥 ∈ ( ℝ* ∖ { -∞ } )
41		dfss3	⊢ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ↔ ∀ 𝑥 ∈ ( 0 [,] +∞ ) 𝑥 ∈ ( ℝ* ∖ { -∞ } ) )
42	40 41	mpbir	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
43		0e0iccpnf	⊢ 0 ∈ ( 0 [,] +∞ )
44	42 43	pm3.2i	⊢ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) )
45		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
46	14 10	ressbas2	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ) )
47	45 46	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
48	14	xrs10	⊢ 0 = ( 0g ‘ ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) )
49		xrex	⊢ ℝ* ∈ V
50		difexg	⊢ ( ℝ* ∈ V → ( ℝ* ∖ { -∞ } ) ∈ V )
51	49 50	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
52	44	simpli	⊢ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } )
53		ressabs	⊢ ( ( ( ℝ* ∖ { -∞ } ) ∈ V ∧ ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ) → ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
54	51 52 53	mp2an	⊢ ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) ) = ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
55	1	eqcomi	⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) = 𝐺
56	54 55	eqtr2i	⊢ 𝐺 = ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ↾s ( 0 [,] +∞ ) )
57	47 48 56	submnd0	⊢ ( ( ( ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) ) ∈ Mnd ∧ 𝐺 ∈ Mnd ) ∧ ( ( 0 [,] +∞ ) ⊆ ( ℝ* ∖ { -∞ } ) ∧ 0 ∈ ( 0 [,] +∞ ) ) ) → 0 = ( 0g ‘ 𝐺 ) )
58	22 44 57	mp2an	⊢ 0 = ( 0g ‘ 𝐺 )
59	19	a1i	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
60	13 58 59 2 3 4	gsumcl	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) ∈ ( 0 [,] +∞ ) )