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 ⊢ Ⅎ 𝑛 𝜑
esumf1o.b ⊢ Ⅎ 𝑛 𝐵
esumf1o.d ⊢ Ⅎ 𝑘 𝐷
esumf1o.a ⊢ Ⅎ 𝑛 𝐴
esumf1o.c ⊢ Ⅎ 𝑛 𝐶
esumf1o.f ⊢ Ⅎ 𝑛 𝐹
esumf1o.1 ⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
esumf1o.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
esumf1o.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
esumf1o.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion esumf1o ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ* 𝑛 ∈ 𝐶 𝐷 )

Proof

Step Hyp Ref Expression
1 esumf1o.0 ⊢ Ⅎ 𝑛 𝜑
2 esumf1o.b ⊢ Ⅎ 𝑛 𝐵
3 esumf1o.d ⊢ Ⅎ 𝑘 𝐷
4 esumf1o.a ⊢ Ⅎ 𝑛 𝐴
5 esumf1o.c ⊢ Ⅎ 𝑛 𝐶
6 esumf1o.f ⊢ Ⅎ 𝑛 𝐹
7 esumf1o.1 ⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
8 esumf1o.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
9 esumf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
10 esumf1o.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
11 esumf1o.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
12 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
13 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
14 13 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
15 xrge0tps ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp
16 15 a1i ⊢ ( 𝜑 → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ TopSp )
17 11 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
18 12 14 16 8 17 9 tsmsf1o ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝐹 ) ) )
19 f1of ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
20 9 19 syl ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
21 20 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 )
22 10 21 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐺 ∈ 𝐴 )
23 22 ex ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐶 → 𝐺 ∈ 𝐴 ) )
24 1 23 ralrimi ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 𝐺 ∈ 𝐴 )
25 5 6 20 feqmptdf ⊢ ( 𝜑 → 𝐹 = ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) )
26 1 10 mpteq2da ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝐶 ↦ 𝐺 ) )
27 25 26 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 𝑛 ∈ 𝐶 ↦ 𝐺 ) )
28 eqidd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
29 2 3 5 4 1 24 27 28 7 fmptcof2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝐹 ) = ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) )
30 29 oveq2d ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝐹 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )
31 18 30 eqtrd ⊢ ( 𝜑 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )
32 31 unieqd ⊢ ( 𝜑 → ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ) )
33 df-esum ⊢ Σ* 𝑘 ∈ 𝐴 𝐵 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
34 df-esum ⊢ Σ* 𝑛 ∈ 𝐶 𝐷 = ∪ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) tsums ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) )
35 32 33 34 3eqtr4g ⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ* 𝑛 ∈ 𝐶 𝐷 )