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	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) )
	esumcocn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumcocn.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	esumcocn.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐽 Cn 𝐽 ) )
	esumcocn.0	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = 0 )
	esumcocn.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) )
Assertion	esumcocn	⊢ ( 𝜑 → ( 𝐶 ‘ Σ^* 𝑘 ∈ 𝐴 𝐵 ) = Σ^* 𝑘 ∈ 𝐴 ( 𝐶 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		esumcocn.j	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) )
2		esumcocn.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		esumcocn.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		esumcocn.1	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐽 Cn 𝐽 ) )
5		esumcocn.0	⊢ ( 𝜑 → ( 𝐶 ‘ 0 ) = 0 )
6		esumcocn.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) )
7		nfv	⊢ Ⅎ 𝑘 𝜑
8		nfcv	⊢ Ⅎ 𝑘 𝐴
9		xrge0tps	⊢ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ TopSp
10		xrge0base	⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
11		xrge0topn	⊢ ( TopOpen ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ) = ( ( ordTop ‘ ≤ ) ↾_t ( 0 [,] +∞ ) )
12	1 11	eqtr4i	⊢ 𝐽 = ( TopOpen ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
13	10 12	tpsuni	⊢ ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ TopSp → ( 0 [,] +∞ ) = ∪ 𝐽 )
14	9 13	ax-mp	⊢ ( 0 [,] +∞ ) = ∪ 𝐽
15	14 14	cnf	⊢ ( 𝐶 ∈ ( 𝐽 Cn 𝐽 ) → 𝐶 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) )
16	4 15	syl	⊢ ( 𝜑 → 𝐶 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) )
18	17 3	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
19		xrge0cmn	⊢ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ CMnd
20	19	a1i	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ CMnd )
21	9	a1i	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ TopSp )
22		cmnmnd	⊢ ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ CMnd → ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd )
23	19 22	ax-mp	⊢ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd
24	23	a1i	⊢ ( 𝜑 → ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd )
25	6	3expib	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) ) )
26	25	ralrimivv	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) )
27		xrge0plusg	⊢ +_𝑒 = ( +_g ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
28		xrge00	⊢ 0 = ( 0_g ‘ ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) )
29	10 10 27 27 28 28	ismhm	⊢ ( 𝐶 ∈ ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) MndHom ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ) ↔ ( ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd ∧ ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd ) ∧ ( 𝐶 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) ∧ ( 𝐶 ‘ 0 ) = 0 ) ) )
30	29	biimpri	⊢ ( ( ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd ∧ ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ∈ Mnd ) ∧ ( 𝐶 : ( 0 [,] +∞ ) ⟶ ( 0 [,] +∞ ) ∧ ∀ 𝑥 ∈ ( 0 [,] +∞ ) ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝐶 ‘ ( 𝑥 +_𝑒 𝑦 ) ) = ( ( 𝐶 ‘ 𝑥 ) +_𝑒 ( 𝐶 ‘ 𝑦 ) ) ∧ ( 𝐶 ‘ 0 ) = 0 ) ) → 𝐶 ∈ ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) MndHom ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
31	24 24 16 26 5 30	syl23anc	⊢ ( 𝜑 → 𝐶 ∈ ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) MndHom ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) ) )
32		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
33	32 3	fmpt3d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
34	7 8 2 3	esumel	⊢ ( 𝜑 → Σ^* 𝑘 ∈ 𝐴 𝐵 ∈ ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) )
35	10 12 12 20 21 20 21 31 4 2 33 34	tsmsmhm	⊢ ( 𝜑 → ( 𝐶 ‘ Σ^* 𝑘 ∈ 𝐴 𝐵 ) ∈ ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) tsums ( 𝐶 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) )
36	16 3	cofmpt	⊢ ( 𝜑 → ( 𝐶 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 ‘ 𝐵 ) ) )
37	36	oveq2d	⊢ ( 𝜑 → ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) tsums ( 𝐶 ∘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) ) = ( ( ℝ^_𝑠 ↾_s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 ‘ 𝐵 ) ) ) )
38	35 37	eleqtrd	⊢ ( 𝜑 → ( 𝐶 ‘ Σ^* 𝑘 ∈ 𝐴 𝐵 ) ∈ ( ( ℝ^*_𝑠 ↾_s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ ( 𝐶 ‘ 𝐵 ) ) ) )
39	7 8 2 18 38	esumid	⊢ ( 𝜑 → Σ^* 𝑘 ∈ 𝐴 ( 𝐶 ‘ 𝐵 ) = ( 𝐶 ‘ Σ^* 𝑘 ∈ 𝐴 𝐵 ) )
40	39	eqcomd	⊢ ( 𝜑 → ( 𝐶 ‘ Σ^* 𝑘 ∈ 𝐴 𝐵 ) = Σ^* 𝑘 ∈ 𝐴 ( 𝐶 ‘ 𝐵 ) )

Metamath Proof Explorer

Theorem esumcocn

Proof