esumcocn

Description: Lemma for esummulc2 and co. Composing with a continuous function preserves extended sums. (Contributed by Thierry Arnoux, 29-Jun-2017)

	Ref	Expression
Hypotheses	esumcocn.j	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
	esumcocn.a	$⊢ φ \to A \in V$
	esumcocn.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
	esumcocn.1	$⊢ φ \to C \in (J Cn J)$
	esumcocn.0	$⊢ φ \to C (0) = 0$
	esumcocn.f	$⊢ (φ \land x \in [0, +∞] \land y \in [0, +∞]) \to C (x +_{𝑒} y) = C (x) +_{𝑒} C (y)$
Assertion	esumcocn	$⊢ φ \to C (\underset{k \in A}{\sum^{}} B) = \underset{k \in A}{\sum^{}} C (B)$

Proof

Step	Hyp	Ref	Expression
1		esumcocn.j	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
2		esumcocn.a	$⊢ φ \to A \in V$
3		esumcocn.b	$⊢ (φ \land k \in A) \to B \in [0, +∞]$
4		esumcocn.1	$⊢ φ \to C \in (J Cn J)$
5		esumcocn.0	$⊢ φ \to C (0) = 0$
6		esumcocn.f	$⊢ (φ \land x \in [0, +∞] \land y \in [0, +∞]) \to C (x +_{𝑒} y) = C (x) +_{𝑒} C (y)$
7		nfv	$⊢ Ⅎ k φ$
8		nfcv	$⊢ \underline{Ⅎ} k A$
9		xrge0tps	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
10		xrge0base	$⊢ [0, +∞] = {Base}_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
11		xrge0topn	$⊢ TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞]) = ordTop (\leq) ↾_{𝑡} [0, +∞]$
12	1 11	eqtr4i	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
13	10 12	tpsuni	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp \to [0, +∞] = ⋃ J$
14	9 13	ax-mp	$⊢ [0, +∞] = ⋃ J$
15	14 14	cnf	$⊢ C \in (J Cn J) \to C : [0, +∞] ⟶ [0, +∞]$
16	4 15	syl	$⊢ φ \to C : [0, +∞] ⟶ [0, +∞]$
17	16	adantr	$⊢ (φ \land k \in A) \to C : [0, +∞] ⟶ [0, +∞]$
18	17 3	ffvelcdmd	$⊢ (φ \land k \in A) \to C (B) \in [0, +∞]$
19		xrge0cmn	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
20	19	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in CMnd$
21	9	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in TopSp$
22		cmnmnd	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in CMnd \to ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in Mnd$
23	19 22	ax-mp	$⊢ ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in Mnd$
24	23	a1i	$⊢ φ \to ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞] \in Mnd$
25	6	3expib	$⊢ φ \to ((x \in [0, +∞] \land y \in [0, +∞]) \to C (x +_{𝑒} y) = C (x) +_{𝑒} C (y))$
26	25	ralrimivv	$⊢ φ \to \forall x \in [0, +∞] \forall y \in [0, +∞] C (x +_{𝑒} y) = C (x) +_{𝑒} C (y)$
27		xrge0plusg	$⊢ +_{𝑒} = +_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
28		xrge00	$⊢ 0 = 0_{(ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])}$
29	10 10 27 27 28 28	ismhm	$⊢ C \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) MndHom (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞])) \leftrightarrow ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in Mnd \land ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in Mnd) \land (C : [0, +∞] ⟶ [0, +∞] \land \forall x \in [0, +∞] \forall y \in [0, +∞] C (x +_{𝑒} y) = C (x) +_{𝑒} C (y) \land C (0) = 0))$
30	29	biimpri	$⊢ ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in Mnd \land ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] \in Mnd) \land (C : [0, +∞] ⟶ [0, +∞] \land \forall x \in [0, +∞] \forall y \in [0, +∞] C (x +_{𝑒} y) = C (x) +_{𝑒} C (y) \land C (0) = 0)) \to C \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) MndHom (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]))$
31	24 24 16 26 5 30	syl23anc	$⊢ φ \to C \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) MndHom (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]))$
32		eqidd	$⊢ φ \to (k \in A ⟼ B) = (k \in A ⟼ B)$
33	32 3	fmpt3d	$⊢ φ \to (k \in A ⟼ B) : A ⟶ [0, +∞]$
34	7 8 2 3	esumel	$⊢ φ \to \underset{k \in A}{\sum^{}} B \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ B))$
35	10 12 12 20 21 20 21 31 4 2 33 34	tsmsmhm	$⊢ φ \to C (\underset{k \in A}{\sum^{}} B) \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (C \circ (k \in A ⟼ B)))$
36	16 3	cofmpt	$⊢ φ \to C \circ (k \in A ⟼ B) = (k \in A ⟼ C (B))$
37	36	oveq2d	$⊢ φ \to (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (C \circ (k \in A ⟼ B)) = (ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ C (B))$
38	35 37	eleqtrd	$⊢ φ \to C (\underset{k \in A}{\sum^{}} B) \in ((ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]) tsums (k \in A ⟼ C (B)))$
39	7 8 2 18 38	esumid	$⊢ φ \to \underset{k \in A}{\sum^{}} C (B) = C (\underset{k \in A}{\sum^{}} B)$
40	39	eqcomd	$⊢ φ \to C (\underset{k \in A}{\sum^{}} B) = \underset{k \in A}{\sum^{}} C (B)$

Metamath Proof Explorer

Theorem esumcocn

Proof