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 
|- F/ n ph
esumf1o.b 
|- F/_ n B
esumf1o.d 
|- F/_ k D
esumf1o.a 
|- F/_ n A
esumf1o.c 
|- F/_ n C
esumf1o.f 
|- F/_ n F
esumf1o.1 
|- ( k = G -> B = D )
esumf1o.2 
|- ( ph -> A e. V )
esumf1o.3 
|- ( ph -> F : C -1-1-onto-> A )
esumf1o.4 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
esumf1o.5 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
Assertion esumf1o 
|- ( ph -> sum* k e. A B = sum* n e. C D )

Proof

Step Hyp Ref Expression
1 esumf1o.0 
 |-  F/ n ph
2 esumf1o.b 
 |-  F/_ n B
3 esumf1o.d 
 |-  F/_ k D
4 esumf1o.a 
 |-  F/_ n A
5 esumf1o.c 
 |-  F/_ n C
6 esumf1o.f 
 |-  F/_ n F
7 esumf1o.1 
 |-  ( k = G -> B = D )
8 esumf1o.2 
 |-  ( ph -> A e. V )
9 esumf1o.3 
 |-  ( ph -> F : C -1-1-onto-> A )
10 esumf1o.4 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) = G )
11 esumf1o.5 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
12 xrge0base 
 |-  ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) )
13 xrge0cmn 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd
14 13 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd )
15 xrge0tps 
 |-  ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp
16 15 a1i 
 |-  ( ph -> ( RR*s |`s ( 0 [,] +oo ) ) e. TopSp )
17 11 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
18 12 14 16 8 17 9 tsmsf1o 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) o. F ) ) )
19 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
20 9 19 syl 
 |-  ( ph -> F : C --> A )
21 20 ffvelrnda 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) e. A )
22 10 21 eqeltrrd 
 |-  ( ( ph /\ n e. C ) -> G e. A )
23 22 ex 
 |-  ( ph -> ( n e. C -> G e. A ) )
24 1 23 ralrimi 
 |-  ( ph -> A. n e. C G e. A )
25 5 6 20 feqmptdf 
 |-  ( ph -> F = ( n e. C |-> ( F ` n ) ) )
26 1 10 mpteq2da 
 |-  ( ph -> ( n e. C |-> ( F ` n ) ) = ( n e. C |-> G ) )
27 25 26 eqtrd 
 |-  ( ph -> F = ( n e. C |-> G ) )
28 eqidd 
 |-  ( ph -> ( k e. A |-> B ) = ( k e. A |-> B ) )
29 2 3 5 4 1 24 27 28 7 fmptcof2 
 |-  ( ph -> ( ( k e. A |-> B ) o. F ) = ( n e. C |-> D ) )
30 29 oveq2d 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( ( k e. A |-> B ) o. F ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( n e. C |-> D ) ) )
31 18 30 eqtrd 
 |-  ( ph -> ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( n e. C |-> D ) ) )
32 31 unieqd 
 |-  ( ph -> U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) ) = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( n e. C |-> D ) ) )
33 df-esum 
 |-  sum* k e. A B = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( k e. A |-> B ) )
34 df-esum 
 |-  sum* n e. C D = U. ( ( RR*s |`s ( 0 [,] +oo ) ) tsums ( n e. C |-> D ) )
35 32 33 34 3eqtr4g 
 |-  ( ph -> sum* k e. A B = sum* n e. C D )