Metamath Proof Explorer

Theorem esumf1o

Description: Re-index an extended sum using a bijection. (Contributed by Thierry Arnoux, 6-Apr-2017)

Ref Expression
Hypotheses esumf1o.0 ⊢ Ⅎ n φ
esumf1o.b ⊢ Ⅎ _ n B
esumf1o.d ⊢ Ⅎ _ k D
esumf1o.a ⊢ Ⅎ _ n A
esumf1o.c ⊢ Ⅎ _ n C
esumf1o.f ⊢ Ⅎ _ n F
esumf1o.1 ⊢ k = G → B = D
esumf1o.2 ⊢ φ → A ∈ V
esumf1o.3 ⊢ φ → F : C ⟶ 1-1 onto A
esumf1o.4 ⊢ φ ∧ n ∈ C → F ⁡ n = G
esumf1o.5 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion esumf1o ⊢ φ → ∑ * k ∈ A B = ∑ * n ∈ C D

Proof

Step Hyp Ref Expression
1 esumf1o.0 ⊢ Ⅎ n φ
2 esumf1o.b ⊢ Ⅎ _ n B
3 esumf1o.d ⊢ Ⅎ _ k D
4 esumf1o.a ⊢ Ⅎ _ n A
5 esumf1o.c ⊢ Ⅎ _ n C
6 esumf1o.f ⊢ Ⅎ _ n F
7 esumf1o.1 ⊢ k = G → B = D
8 esumf1o.2 ⊢ φ → A ∈ V
9 esumf1o.3 ⊢ φ → F : C ⟶ 1-1 onto A
10 esumf1o.4 ⊢ φ ∧ n ∈ C → F ⁡ n = G
11 esumf1o.5 ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
12 xrge0base ⊢ 0 +∞ = Base ℝ 𝑠 * ↾ 𝑠 0 +∞
13 xrge0cmn ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
14 13 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ CMnd
15 xrge0tps ⊢ ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
16 15 a1i ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ ∈ TopSp
17 11 fmpttd ⊢ φ → k ∈ A ⟼ B : A ⟶ 0 +∞
18 12 14 16 8 17 9 tsmsf1o ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B ∘ F
19 f1of ⊢ F : C ⟶ 1-1 onto A → F : C ⟶ A
20 9 19 syl ⊢ φ → F : C ⟶ A
21 20 ffvelcdmda ⊢ φ ∧ n ∈ C → F ⁡ n ∈ A
22 10 21 eqeltrrd ⊢ φ ∧ n ∈ C → G ∈ A
23 22 ex ⊢ φ → n ∈ C → G ∈ A
24 1 23 ralrimi ⊢ φ → ∀ n ∈ C G ∈ A
25 5 6 20 feqmptdf ⊢ φ → F = n ∈ C ⟼ F ⁡ n
26 1 10 mpteq2da ⊢ φ → n ∈ C ⟼ F ⁡ n = n ∈ C ⟼ G
27 25 26 eqtrd ⊢ φ → F = n ∈ C ⟼ G
28 eqidd ⊢ φ → k ∈ A ⟼ B = k ∈ A ⟼ B
29 2 3 5 4 1 24 27 28 7 fmptcof2 ⊢ φ → k ∈ A ⟼ B ∘ F = n ∈ C ⟼ D
30 29 oveq2d ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B ∘ F = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums n ∈ C ⟼ D
31 18 30 eqtrd ⊢ φ → ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums n ∈ C ⟼ D
32 31 unieqd ⊢ φ → ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums n ∈ C ⟼ D
33 df-esum ⊢ ∑ * k ∈ A B = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums k ∈ A ⟼ B
34 df-esum ⊢ ∑ * n ∈ C D = ⋃ ℝ 𝑠 * ↾ 𝑠 0 +∞ tsums n ∈ C ⟼ D
35 32 33 34 3eqtr4g ⊢ φ → ∑ * k ∈ A B = ∑ * n ∈ C D