Metamath Proof Explorer

Theorem 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 ⁡ ≤ ↾ 𝑡 0 +∞
esumcocn.a ⊢ φ → A ∈ V
esumcocn.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
esumcocn.1 ⊢ φ → C ∈ J Cn J
esumcocn.0 ⊢ φ → C ⁡ 0 = 0
esumcocn.f ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → C ⁡ x + 𝑒 y = C ⁡ x + 𝑒 C ⁡ y
Assertion esumcocn ⊢ φ → C ⁡ ∑ * k ∈ A B = ∑ * k ∈ A C ⁡ B

Proof

Step Hyp Ref Expression
1 esumcocn.j ⊢ J = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
2 esumcocn.a ⊢ φ → A ∈ V
3 esumcocn.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
4 esumcocn.1 ⊢ φ → C ∈ J Cn J
5 esumcocn.0 ⊢ φ → C ⁡ 0 = 0
6 esumcocn.f ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → C ⁡ x + 𝑒 y = C ⁡ x + 𝑒 C ⁡ y
7 nfv ⊢ Ⅎ k φ
8 nfcv ⊢ Ⅎ _ k A
9 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
10 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
11 xrge0topn ⊢ TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞ = ordTop ⁡ ≤ ↾ 𝑡 0 +∞
12 1 11 eqtr4i ⊢ J = TopOpen ⁡ ℝ 𝑠 * ↾ 𝑠 0 +∞
13 10 12 tpsuni ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp → 0 +∞ = ⋃ J
14 9 13 ax-mp ⊢ 0 +∞ = ⋃ J
15 14 14 cnf ⊢ C ∈ J Cn J → C : 0 +∞ ⟶ 0 +∞
16 4 15 syl ⊢ φ → C : 0 +∞ ⟶ 0 +∞
17 16 adantr ⊢ φ ∧ k ∈ A → C : 0 +∞ ⟶ 0 +∞
18 17 3 ffvelrnd ⊢ φ ∧ k ∈ A → C ⁡ B ∈ 0 +∞
19 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
20 19 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
21 9 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
22 cmnmnd ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
23 19 22 ax-mp ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
24 23 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd
25 6 3expib ⊢ φ → x ∈ 0 +∞ ∧ y ∈ 0 +∞ → C ⁡ x + 𝑒 y = C ⁡ x + 𝑒 C ⁡ y
26 25 ralrimivv ⊢ φ → ∀ x ∈ 0 +∞ ∀ y ∈ 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 ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ MndHom ℝ 𝑠 * ↾ 𝑠 0 +∞ ↔ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ C : 0 +∞ ⟶ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ C ⁡ x + 𝑒 y = C ⁡ x + 𝑒 C ⁡ y ∧ C ⁡ 0 = 0
30 29 biimpri ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ Mnd ∧ C : 0 +∞ ⟶ 0 +∞ ∧ ∀ x ∈ 0 +∞ ∀ y ∈ 0 +∞ C ⁡ x + 𝑒 y = C ⁡ x + 𝑒 C ⁡ y ∧ C ⁡ 0 = 0 → C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ MndHom ℝ 𝑠 * ↾ 𝑠 0 +∞
31 24 24 16 26 5 30 syl23anc ⊢ φ → C ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ MndHom ℝ 𝑠 * ↾ 𝑠 0 +∞
32 eqidd ⊢ φ → k ∈ A ⟼ B = k ∈ A ⟼ B
33 32 3 fmpt3d ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
34 7 8 2 3 esumel ⊢ φ → ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
35 10 12 12 20 21 20 21 31 4 2 33 34 tsmsmhm ⊢ φ → C ⁡ ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums C ∘ k ∈ A ⟼ B
36 16 3 cofmpt ⊢ φ → C ∘ k ∈ A ⟼ B = k ∈ A ⟼ C ⁡ B
37 36 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums C ∘ k ∈ A ⟼ B = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C ⁡ B
38 35 37 eleqtrd ⊢ φ → C ⁡ ∑ * k ∈ A B ∈ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ C ⁡ B
39 7 8 2 18 38 esumid ⊢ φ → ∑ * k ∈ A C ⁡ B = C ⁡ ∑ * k ∈ A B
40 39 eqcomd ⊢ φ → C ⁡ ∑ * k ∈ A B = ∑ * k ∈ A C ⁡ B