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 ffvelrnda ( ( 𝜑𝑛𝐶 ) → ( 𝐹𝑛 ) ∈ 𝐴 )
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 ( 𝜑 → Σ* 𝑘𝐴 𝐵 = Σ* 𝑛𝐶 𝐷 )