sge0tsms

Description: sum^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0tsms.g	$⊢ G = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
	sge0tsms.x	$⊢ φ \to X \in V$
	sge0tsms.f	$⊢ φ \to F : X ⟶ [0, +∞]$
Assertion	sge0tsms	$⊢ φ \to sum^(F) \in (G tsums F)$

Proof

Step	Hyp	Ref	Expression
1		sge0tsms.g	$⊢ G = ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]$
2		sge0tsms.x	$⊢ φ \to X \in V$
3		sge0tsms.f	$⊢ φ \to F : X ⟶ [0, +∞]$
4		eqid	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)$
5	4	a1i	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)$
6		xrltso	$⊢ < Or ℝ^{*}$
7	6	supex	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) \in V$
8	7	a1i	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) \in V$
9		elsng	$⊢ sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) \in V \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) \in \{sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)\} \leftrightarrow sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <))$
10	8 9	syl	$⊢ φ \to (sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) \in \{sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)\} \leftrightarrow sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <))$
11	5 10	mpbird	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) \in \{sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)\}$
12	2	adantr	$⊢ (φ \land +∞ \in ran F) \to X \in V$
13	3	adantr	$⊢ (φ \land +∞ \in ran F) \to F : X ⟶ [0, +∞]$
14		simpr	$⊢ (φ \land +∞ \in ran F) \to +∞ \in ran F$
15	12 13 14	sge0pnfval	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = +∞$
16	3	ffnd	$⊢ φ \to F Fn X$
17	16	adantr	$⊢ (φ \land +∞ \in ran F) \to F Fn X$
18		fvelrnb	$⊢ F Fn X \to (+∞ \in ran F \leftrightarrow \exists y \in X F (y) = +∞)$
19	17 18	syl	$⊢ (φ \land +∞ \in ran F) \to (+∞ \in ran F \leftrightarrow \exists y \in X F (y) = +∞)$
20	14 19	mpbid	$⊢ (φ \land +∞ \in ran F) \to \exists y \in X F (y) = +∞$
21		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
22		simpr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in (𝒫 X \cap Fin)$
23	3	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
24		elinel1	$⊢ x \in (𝒫 X \cap Fin) \to x \in 𝒫 X$
25		elpwi	$⊢ x \in 𝒫 X \to x \subseteq X$
26	24 25	syl	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
27	26	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
28		fssres	$⊢ (F : X ⟶ [0, +∞] \land x \subseteq X) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
29	23 27 28	syl2anc	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
30		elinel2	$⊢ x \in (𝒫 X \cap Fin) \to x \in Fin$
31	30	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
32		0red	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to 0 \in ℝ$
33	29 31 32	fdmfifsupp	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to {finSupp}_{0} (({F ↾}_{x}))$
34	1 22 29 33	gsumge0cl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{G} ({F ↾}_{x}) \in [0, +∞]$
35	21 34	sseldi	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to \sum_{G} ({F ↾}_{x}) \in ℝ^{*}$
36	35	ralrimiva	$⊢ φ \to \forall x \in (𝒫 X \cap Fin) \sum_{G} ({F ↾}_{x}) \in ℝ^{*}$
37	36	3ad2ant1	$⊢ (φ \land y \in X \land F (y) = +∞) \to \forall x \in (𝒫 X \cap Fin) \sum_{G} ({F ↾}_{x}) \in ℝ^{*}$
38		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x}))$
39	38	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) \sum_{G} ({F ↾}_{x}) \in ℝ^{} \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) \subseteq ℝ^{}$
40	37 39	syl	$⊢ (φ \land y \in X \land F (y) = +∞) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) \subseteq ℝ^{*}$
41		snelpwi	$⊢ y \in X \to \{y\} \in 𝒫 X$
42		snfi	$⊢ \{y\} \in Fin$
43	42	a1i	$⊢ y \in X \to \{y\} \in Fin$
44	41 43	elind	$⊢ y \in X \to \{y\} \in (𝒫 X \cap Fin)$
45	44	3ad2ant2	$⊢ (φ \land y \in X \land F (y) = +∞) \to \{y\} \in (𝒫 X \cap Fin)$
46	3	adantr	$⊢ (φ \land y \in X) \to F : X ⟶ [0, +∞]$
47		snssi	$⊢ y \in X \to \{y\} \subseteq X$
48	47	adantl	$⊢ (φ \land y \in X) \to \{y\} \subseteq X$
49	46 48	fssresd	$⊢ (φ \land y \in X) \to ({F ↾}_{\{y\}}) : \{y\} ⟶ [0, +∞]$
50	49	feqmptd	$⊢ (φ \land y \in X) \to {F ↾}_{\{y\}} = (x \in \{y\} ⟼ ({F ↾}_{\{y\}}) (x))$
51		fvres	$⊢ x \in \{y\} \to ({F ↾}_{\{y\}}) (x) = F (x)$
52	51	mpteq2ia	$⊢ (x \in \{y\} ⟼ ({F ↾}_{\{y\}}) (x)) = (x \in \{y\} ⟼ F (x))$
53	52	a1i	$⊢ (φ \land y \in X) \to (x \in \{y\} ⟼ ({F ↾}_{\{y\}}) (x)) = (x \in \{y\} ⟼ F (x))$
54	50 53	eqtrd	$⊢ (φ \land y \in X) \to {F ↾}_{\{y\}} = (x \in \{y\} ⟼ F (x))$
55	54	oveq2d	$⊢ (φ \land y \in X) \to \sum_{G} ({F ↾}_{\{y\}}) = \underset{x \in \{y\}}{\sum_{G}} F (x)$
56	55	3adant3	$⊢ (φ \land y \in X \land F (y) = +∞) \to \sum_{G} ({F ↾}_{\{y\}}) = \underset{x \in \{y\}}{\sum_{G}} F (x)$
57		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
58	1 57	eqeltri	$⊢ G \in CMnd$
59		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
60	58 59	ax-mp	$⊢ G \in Mnd$
61	60	a1i	$⊢ (φ \land y \in X \land F (y) = +∞) \to G \in Mnd$
62		simp2	$⊢ (φ \land y \in X \land F (y) = +∞) \to y \in X$
63	3	ffvelrnda	$⊢ (φ \land y \in X) \to F (y) \in [0, +∞]$
64	63	3adant3	$⊢ (φ \land y \in X \land F (y) = +∞) \to F (y) \in [0, +∞]$
65		df-ss	$⊢ [0, +∞] \subseteq ℝ^{} \leftrightarrow [0, +∞] \cap ℝ^{} = [0, +∞]$
66	21 65	mpbi	$⊢ [0, +∞] \cap ℝ^{*} = [0, +∞]$
67	66	eqcomi	$⊢ [0, +∞] = [0, +∞] \cap ℝ^{*}$
68		ovex	$⊢ [0, +∞] \in V$
69		xrsbas	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
70	1 69	ressbas	$⊢ [0, +∞] \in V \to [0, +∞] \cap ℝ^{*} = {Base}_{G}$
71	68 70	ax-mp	$⊢ [0, +∞] \cap ℝ^{*} = {Base}_{G}$
72	67 71	eqtri	$⊢ [0, +∞] = {Base}_{G}$
73		fveq2	$⊢ x = y \to F (x) = F (y)$
74	72 73	gsumsn	$⊢ (G \in Mnd \land y \in X \land F (y) \in [0, +∞]) \to \underset{x \in \{y\}}{\sum_{G}} F (x) = F (y)$
75	61 62 64 74	syl3anc	$⊢ (φ \land y \in X \land F (y) = +∞) \to \underset{x \in \{y\}}{\sum_{G}} F (x) = F (y)$
76		simp3	$⊢ (φ \land y \in X \land F (y) = +∞) \to F (y) = +∞$
77	56 75 76	3eqtrrd	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ = \sum_{G} ({F ↾}_{\{y\}})$
78		reseq2	$⊢ x = \{y\} \to {F ↾}_{x} = {F ↾}_{\{y\}}$
79	78	oveq2d	$⊢ x = \{y\} \to \sum_{G} ({F ↾}_{x}) = \sum_{G} ({F ↾}_{\{y\}})$
80	79	rspceeqv	$⊢ (\{y\} \in (𝒫 X \cap Fin) \land +∞ = \sum_{G} ({F ↾}_{\{y\}})) \to \exists x \in (𝒫 X \cap Fin) +∞ = \sum_{G} ({F ↾}_{x})$
81	45 77 80	syl2anc	$⊢ (φ \land y \in X \land F (y) = +∞) \to \exists x \in (𝒫 X \cap Fin) +∞ = \sum_{G} ({F ↾}_{x})$
82		pnfxr	$⊢ +∞ \in ℝ^{*}$
83	82	a1i	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ \in ℝ^{*}$
84	38	elrnmpt	$⊢ +∞ \in ℝ^{*} \to (+∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) +∞ = \sum_{G} ({F ↾}_{x}))$
85	83 84	syl	$⊢ (φ \land y \in X \land F (y) = +∞) \to (+∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) +∞ = \sum_{G} ({F ↾}_{x}))$
86	81 85	mpbird	$⊢ (φ \land y \in X \land F (y) = +∞) \to +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x}))$
87		supxrpnf	$⊢ (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) \subseteq ℝ^{} \land +∞ \in ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x}))) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) = +∞$
88	40 86 87	syl2anc	$⊢ (φ \land y \in X \land F (y) = +∞) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) = +∞$
89	88	3exp	$⊢ φ \to (y \in X \to (F (y) = +∞ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) = +∞))$
90	89	adantr	$⊢ (φ \land +∞ \in ran F) \to (y \in X \to (F (y) = +∞ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) = +∞))$
91	90	rexlimdv	$⊢ (φ \land +∞ \in ran F) \to (\exists y \in X F (y) = +∞ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) = +∞)$
92	20 91	mpd	$⊢ (φ \land +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <) = +∞$
93	15 92	eqtr4d	$⊢ (φ \land +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)$
94	2	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to X \in V$
95	3	adantr	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞]$
96		simpr	$⊢ (φ \land \neg +∞ \in ran F) \to \neg +∞ \in ran F$
97	95 96	fge0iccico	$⊢ (φ \land \neg +∞ \in ran F) \to F : X ⟶ [0, +∞)$
98	94 97	sge0reval	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{*} <)$
99	23 27	feqresmpt	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to {F ↾}_{x} = (y \in x ⟼ F (y))$
100	99	adantlr	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to {F ↾}_{x} = (y \in x ⟼ F (y))$
101	100	oveq2d	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \sum_{G} ({F ↾}_{x}) = \underset{y \in x}{\sum_{G}} F (y)$
102	1	fveq2i	$⊢ +_{G} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
103		eqid	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]$
104		xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
105	103 104	ressplusg	$⊢ [0, +∞] \in V \to +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
106	68 105	ax-mp	$⊢ +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
107	106	eqcomi	$⊢ +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])} = +_{𝑒}$
108	102 107	eqtr2i	$⊢ +_{𝑒} = +_{G}$
109	1	oveq1i	$⊢ G ↾_{𝑠} [0, +∞) = (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]) ↾_{𝑠} [0, +∞)$
110		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
111	68 110	pm3.2i	$⊢ ([0, +∞] \in V \land [0, +∞) \subseteq [0, +∞])$
112		ressabs	$⊢ ([0, +∞] \in V \land [0, +∞) \subseteq [0, +∞]) \to (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) ↾_{𝑠} [0, +∞) = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞)$
113	111 112	ax-mp	$⊢ (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) ↾_{𝑠} [0, +∞) = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞)$
114	109 113	eqtr2i	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞) = G ↾_{𝑠} [0, +∞)$
115	58	elexi	$⊢ G \in V$
116	115	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to G \in V$
117		simpr	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to x \in (𝒫 X \cap Fin)$
118	110	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to [0, +∞) \subseteq [0, +∞]$
119		0xr	$⊢ 0 \in ℝ^{*}$
120	119	a1i	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to 0 \in ℝ^{*}$
121	82	a1i	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to +∞ \in ℝ^{*}$
122	95	ad2antrr	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F : X ⟶ [0, +∞]$
123	26	sselda	$⊢ (x \in (𝒫 X \cap Fin) \land y \in x) \to y \in X$
124	123	adantll	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
125	122 124	ffvelrnd	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞]$
126	21 125	sseldi	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ^{*}$
127		iccgelb	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land F (y) \in [0, +∞]) \to 0 \leq F (y)$
128	120 121 125 127	syl3anc	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to 0 \leq F (y)$
129		id	$⊢ F (y) = +∞ \to F (y) = +∞$
130	129	eqcomd	$⊢ F (y) = +∞ \to +∞ = F (y)$
131	130	adantl	$⊢ (((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \land F (y) = +∞) \to +∞ = F (y)$
132	3	ffund	$⊢ φ \to Fun F$
133	132	ad2antrr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to Fun F$
134	22 123	sylan	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in X$
135	3	fdmd	$⊢ φ \to dom F = X$
136	135	eqcomd	$⊢ φ \to X = dom F$
137	136	ad2antrr	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to X = dom F$
138	134 137	eleqtrd	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to y \in dom F$
139		fvelrn	$⊢ (Fun F \land y \in dom F) \to F (y) \in ran F$
140	133 138 139	syl2anc	$⊢ ((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ran F$
141	140	adantr	$⊢ (((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \land F (y) = +∞) \to F (y) \in ran F$
142	131 141	eqeltrd	$⊢ (((φ \land x \in (𝒫 X \cap Fin)) \land y \in x) \land F (y) = +∞) \to +∞ \in ran F$
143	142	adantl3r	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land F (y) = +∞) \to +∞ \in ran F$
144	96	ad3antrrr	$⊢ ((((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \land F (y) = +∞) \to \neg +∞ \in ran F$
145	143 144	pm2.65da	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to \neg F (y) = +∞$
146	145	neqned	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \neq +∞$
147		ge0xrre	$⊢ (F (y) \in [0, +∞] \land F (y) \neq +∞) \to F (y) \in ℝ$
148	125 146 147	syl2anc	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℝ$
149	148	ltpnfd	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) < +∞$
150	120 121 126 128 149	elicod	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in [0, +∞)$
151		eqid	$⊢ (y \in x ⟼ F (y)) = (y \in x ⟼ F (y))$
152	150 151	fmptd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to (y \in x ⟼ F (y)) : x ⟶ [0, +∞)$
153		0e0icopnf	$⊢ 0 \in [0, +∞)$
154	153	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to 0 \in [0, +∞)$
155		eliccxr	$⊢ y \in [0, +∞] \to y \in ℝ^{*}$
156		xaddid2	$⊢ y \in ℝ^{*} \to 0 +_{𝑒} y = y$
157		xaddid1	$⊢ y \in ℝ^{*} \to y +_{𝑒} 0 = y$
158	156 157	jca	$⊢ y \in ℝ^{*} \to (0 +_{𝑒} y = y \land y +_{𝑒} 0 = y)$
159	155 158	syl	$⊢ y \in [0, +∞] \to (0 +_{𝑒} y = y \land y +_{𝑒} 0 = y)$
160	159	adantl	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in [0, +∞]) \to (0 +_{𝑒} y = y \land y +_{𝑒} 0 = y)$
161	72 108 114 116 117 118 152 154 160	gsumress	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{G}} F (y) = \underset{y \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞)}} F (y)$
162		rege0subm	$⊢ [0, +∞) \in SubMnd (ℂ_{fld})$
163	162	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to [0, +∞) \in SubMnd (ℂ_{fld})$
164		eqid	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) = ℂ_{fld} ↾_{𝑠} [0, +∞)$
165	117 163 152 164	gsumsubm	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℂ_{fld}}} F (y) = \underset{y \in x}{\sum_{ℂ_{fld} ↾_{𝑠} [0, +∞)}} F (y)$
166		eqidd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℂ_{fld} ↾_{𝑠} [0, +∞)}} F (y) = \underset{y \in x}{\sum_{ℂ_{fld} ↾_{𝑠} [0, +∞)}} F (y)$
167		vex	$⊢ x \in V$
168	167	mptex	$⊢ (y \in x ⟼ F (y)) \in V$
169	168	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to (y \in x ⟼ F (y)) \in V$
170		ovexd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to ℂ_{fld} ↾_{𝑠} [0, +∞) \in V$
171		ovexd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞) \in V$
172		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
173		ax-resscn	$⊢ ℝ \subseteq ℂ$
174	172 173	sstri	$⊢ [0, +∞) \subseteq ℂ$
175		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
176	164 175	ressbas2	$⊢ [0, +∞) \subseteq ℂ \to [0, +∞) = {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
177	174 176	ax-mp	$⊢ [0, +∞) = {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
178	177	eqcomi	$⊢ {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = [0, +∞)$
179	110 21	sstri	$⊢ [0, +∞) \subseteq ℝ^{*}$
180		eqid	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞) = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞)$
181	180 69	ressbas2	$⊢ [0, +∞) \subseteq ℝ^{} \to [0, +∞) = {Base}_{(ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞))}$
182	179 181	ax-mp	$⊢ [0, +∞) = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))}$
183	178 182	eqtri	$⊢ {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))}$
184	183	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))}$
185		rge0srg	$⊢ ℂ_{fld} ↾_{𝑠} [0, +∞) \in SRing$
186	185	a1i	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to ℂ_{fld} ↾_{𝑠} [0, +∞) \in SRing$
187		simpl	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
188		simpr	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
189		eqid	$⊢ {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
190		eqid	$⊢ +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
191	189 190	srgacl	$⊢ (ℂ_{fld} ↾_{𝑠} [0, +∞) \in SRing \land s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
192	186 187 188 191	syl3anc	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
193	192	adantl	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))})) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
194	172	a1i	$⊢ s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to [0, +∞) \subseteq ℝ$
195		id	$⊢ s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
196	195 178	eleqtrdi	$⊢ s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to s \in [0, +∞)$
197	194 196	sseldd	$⊢ s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to s \in ℝ$
198	197	adantr	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to s \in ℝ$
199	172	a1i	$⊢ t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to [0, +∞) \subseteq ℝ$
200		id	$⊢ t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
201	200 178	eleqtrdi	$⊢ t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to t \in [0, +∞)$
202	199 201	sseldd	$⊢ t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to t \in ℝ$
203	202	adantl	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to t \in ℝ$
204		rexadd	$⊢ (s \in ℝ \land t \in ℝ) \to s +_{𝑒} t = s + t$
205	204	eqcomd	$⊢ (s \in ℝ \land t \in ℝ) \to s + t = s +_{𝑒} t$
206	162	elexi	$⊢ [0, +∞) \in V$
207		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
208	164 207	ressplusg	$⊢ [0, +∞) \in V \to + = +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
209	206 208	ax-mp	$⊢ + = +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
210	209 207	eqtr3i	$⊢ +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = +_{ℂ_{fld}}$
211	210 207	eqtr4i	$⊢ +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} = +$
212	211	oveqi	$⊢ s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t = s + t$
213	212	a1i	$⊢ (s \in ℝ \land t \in ℝ) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t = s + t$
214	180 104	ressplusg	$⊢ [0, +∞) \in V \to +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))}$
215	206 214	ax-mp	$⊢ +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))}$
216	215	eqcomi	$⊢ +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} = +_{𝑒}$
217	216	oveqi	$⊢ s +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} t = s +_{𝑒} t$
218	217	a1i	$⊢ (s \in ℝ \land t \in ℝ) \to s +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} t = s +_{𝑒} t$
219	205 213 218	3eqtr4d	$⊢ (s \in ℝ \land t \in ℝ) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t = s +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} t$
220	198 203 219	syl2anc	$⊢ (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t = s +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} t$
221	220	adantl	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land (s \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \land t \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))})) \to s +_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} t = s +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞))} t$
222		funmpt	$⊢ Fun (y \in x ⟼ F (y))$
223	222	a1i	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to Fun (y \in x ⟼ F (y))$
224	150 177	eleqtrdi	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
225	224	ralrimiva	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \forall y \in x F (y) \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
226	151	rnmptss	$⊢ \forall y \in x F (y) \in {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))} \to ran (y \in x ⟼ F (y)) \subseteq {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
227	225 226	syl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to ran (y \in x ⟼ F (y)) \subseteq {Base}_{(ℂ_{fld} ↾_{𝑠} [0, +∞))}$
228	169 170 171 184 193 221 223 227	gsumpropd2	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℂ_{fld} ↾_{𝑠} [0, +∞)}} F (y) = \underset{y \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞)}} F (y)$
229	165 166 228	3eqtrd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℂ_{fld}}} F (y) = \underset{y \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞)}} F (y)$
230	30	adantl	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to x \in Fin$
231	148	recnd	$⊢ (((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \land y \in x) \to F (y) \in ℂ$
232	230 231	gsumfsum	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℂ_{fld}}} F (y) = \sum_{y \in x} F (y)$
233	229 232	eqtr3d	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \underset{y \in x}{\sum_{ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞)}} F (y) = \sum_{y \in x} F (y)$
234	101 161 233	3eqtrrd	$⊢ ((φ \land \neg +∞ \in ran F) \land x \in (𝒫 X \cap Fin)) \to \sum_{y \in x} F (y) = \sum_{G} ({F ↾}_{x})$
235	234	mpteq2dva	$⊢ (φ \land \neg +∞ \in ran F) \to (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x}))$
236	235	rneqd	$⊢ (φ \land \neg +∞ \in ran F) \to ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) = ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x}))$
237	236	supeq1d	$⊢ (φ \land \neg +∞ \in ran F) \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{y \in x} F (y)) ℝ^{} <) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)$
238	98 237	eqtrd	$⊢ (φ \land \neg +∞ \in ran F) \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)$
239	93 238	pm2.61dan	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)$
240	1 2 3 4	xrge0tsms	$⊢ φ \to G tsums F = \{sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{*} <)\}$
241	239 240	eleq12d	$⊢ φ \to (sum^(F) \in (G tsums F) \leftrightarrow sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <) \in \{sup (ran (x \in (𝒫 X \cap Fin) ⟼ \sum_{G} ({F ↾}_{x})) ℝ^{} <)\})$
242	11 241	mpbird	$⊢ φ \to sum^(F) \in (G tsums F)$

Metamath Proof Explorer

Theorem sge0tsms

Proof