Metamath Proof Explorer

Theorem fsumf1o

Description: Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses fsumf1o.1 
|- ( k = G -> B = D )
fsumf1o.2 
|- ( ph -> C e. Fin )
fsumf1o.3 
|- ( ph -> F : C -1-1-onto-> A )
fsumf1o.4 
|- ( ( ph /\ n e. C ) -> ( F ` n ) = G )
fsumf1o.5 
|- ( ( ph /\ k e. A ) -> B e. CC )
Assertion fsumf1o 
|- ( ph -> sum_ k e. A B = sum_ n e. C D )

Proof

Step Hyp Ref Expression
1 fsumf1o.1 
 |-  ( k = G -> B = D )
2 fsumf1o.2 
 |-  ( ph -> C e. Fin )
3 fsumf1o.3 
 |-  ( ph -> F : C -1-1-onto-> A )
4 fsumf1o.4 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) = G )
5 fsumf1o.5 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
6 sum0 
 |-  sum_ k e. (/) B = 0
7 f1oeq2 
 |-  ( C = (/) -> ( F : C -1-1-onto-> A <-> F : (/) -1-1-onto-> A ) )
8 3 7 syl5ibcom 
 |-  ( ph -> ( C = (/) -> F : (/) -1-1-onto-> A ) )
9 8 imp 
 |-  ( ( ph /\ C = (/) ) -> F : (/) -1-1-onto-> A )
10 f1ofo 
 |-  ( F : (/) -1-1-onto-> A -> F : (/) -onto-> A )
11 fo00 
 |-  ( F : (/) -onto-> A <-> ( F = (/) /\ A = (/) ) )
12 11 simprbi 
 |-  ( F : (/) -onto-> A -> A = (/) )
13 9 10 12 3syl 
 |-  ( ( ph /\ C = (/) ) -> A = (/) )
14 13 sumeq1d 
 |-  ( ( ph /\ C = (/) ) -> sum_ k e. A B = sum_ k e. (/) B )
15 simpr 
 |-  ( ( ph /\ C = (/) ) -> C = (/) )
16 15 sumeq1d 
 |-  ( ( ph /\ C = (/) ) -> sum_ n e. C D = sum_ n e. (/) D )
17 sum0 
 |-  sum_ n e. (/) D = 0
18 16 17 syl6eq 
 |-  ( ( ph /\ C = (/) ) -> sum_ n e. C D = 0 )
19 6 14 18 3eqtr4a 
 |-  ( ( ph /\ C = (/) ) -> sum_ k e. A B = sum_ n e. C D )
20 19 ex 
 |-  ( ph -> ( C = (/) -> sum_ k e. A B = sum_ n e. C D ) )
21 2fveq3 
 |-  ( m = ( f ` n ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
22 simprl 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( # ` C ) e. NN )
23 simprr 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> f : ( 1 ... ( # ` C ) ) -1-1-onto-> C )
24 f1of 
 |-  ( F : C -1-1-onto-> A -> F : C --> A )
25 3 24 syl 
 |-  ( ph -> F : C --> A )
26 25 ffvelrnda 
 |-  ( ( ph /\ m e. C ) -> ( F ` m ) e. A )
27 5 fmpttd 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
28 27 ffvelrnda 
 |-  ( ( ph /\ ( F ` m ) e. A ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
29 26 28 syldan 
 |-  ( ( ph /\ m e. C ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
30 29 adantlr 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. C ) -> ( ( k e. A |-> B ) ` ( F ` m ) ) e. CC )
31 f1oco 
 |-  ( ( F : C -1-1-onto-> A /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A )
32 3 23 31 syl2an2r 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A )
33 f1of 
 |-  ( ( F o. f ) : ( 1 ... ( # ` C ) ) -1-1-onto-> A -> ( F o. f ) : ( 1 ... ( # ` C ) ) --> A )
34 32 33 syl 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( F o. f ) : ( 1 ... ( # ` C ) ) --> A )
35 fvco3 
 |-  ( ( ( F o. f ) : ( 1 ... ( # ` C ) ) --> A /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
36 34 35 sylan 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
37 f1of 
 |-  ( f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> f : ( 1 ... ( # ` C ) ) --> C )
38 37 ad2antll 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> f : ( 1 ... ( # ` C ) ) --> C )
39 fvco3 
 |-  ( ( f : ( 1 ... ( # ` C ) ) --> C /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( F o. f ) ` n ) = ( F ` ( f ` n ) ) )
40 38 39 sylan 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( F o. f ) ` n ) = ( F ` ( f ` n ) ) )
41 40 fveq2d 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
42 36 41 eqtrd 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ n e. ( 1 ... ( # ` C ) ) ) -> ( ( ( k e. A |-> B ) o. ( F o. f ) ) ` n ) = ( ( k e. A |-> B ) ` ( F ` ( f ` n ) ) ) )
43 21 22 23 30 42 fsum 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> sum_ m e. C ( ( k e. A |-> B ) ` ( F ` m ) ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. ( F o. f ) ) ) ` ( # ` C ) ) )
44 25 ffvelrnda 
 |-  ( ( ph /\ n e. C ) -> ( F ` n ) e. A )
45 4 44 eqeltrrd 
 |-  ( ( ph /\ n e. C ) -> G e. A )
46 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
47 1 46 fvmpti 
 |-  ( G e. A -> ( ( k e. A |-> B ) ` G ) = ( _I ` D ) )
48 45 47 syl 
 |-  ( ( ph /\ n e. C ) -> ( ( k e. A |-> B ) ` G ) = ( _I ` D ) )
49 4 fveq2d 
 |-  ( ( ph /\ n e. C ) -> ( ( k e. A |-> B ) ` ( F ` n ) ) = ( ( k e. A |-> B ) ` G ) )
50 eqid 
 |-  ( n e. C |-> D ) = ( n e. C |-> D )
51 50 fvmpt2i 
 |-  ( n e. C -> ( ( n e. C |-> D ) ` n ) = ( _I ` D ) )
52 51 adantl 
 |-  ( ( ph /\ n e. C ) -> ( ( n e. C |-> D ) ` n ) = ( _I ` D ) )
53 48 49 52 3eqtr4rd 
 |-  ( ( ph /\ n e. C ) -> ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) )
54 53 ralrimiva 
 |-  ( ph -> A. n e. C ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) )
55 nffvmpt1 
 |-  F/_ n ( ( n e. C |-> D ) ` m )
56 55 nfeq1 
 |-  F/ n ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) )
57 fveq2 
 |-  ( n = m -> ( ( n e. C |-> D ) ` n ) = ( ( n e. C |-> D ) ` m ) )
58 2fveq3 
 |-  ( n = m -> ( ( k e. A |-> B ) ` ( F ` n ) ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
59 57 58 eqeq12d 
 |-  ( n = m -> ( ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) <-> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) ) )
60 56 59 rspc 
 |-  ( m e. C -> ( A. n e. C ( ( n e. C |-> D ) ` n ) = ( ( k e. A |-> B ) ` ( F ` n ) ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) ) )
61 54 60 mpan9 
 |-  ( ( ph /\ m e. C ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
62 61 adantlr 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. C ) -> ( ( n e. C |-> D ) ` m ) = ( ( k e. A |-> B ) ` ( F ` m ) ) )
63 62 sumeq2dv 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> sum_ m e. C ( ( n e. C |-> D ) ` m ) = sum_ m e. C ( ( k e. A |-> B ) ` ( F ` m ) ) )
64 fveq2 
 |-  ( m = ( ( F o. f ) ` n ) -> ( ( k e. A |-> B ) ` m ) = ( ( k e. A |-> B ) ` ( ( F o. f ) ` n ) ) )
65 27 adantr 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> ( k e. A |-> B ) : A --> CC )
66 65 ffvelrnda 
 |-  ( ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) /\ m e. A ) -> ( ( k e. A |-> B ) ` m ) e. CC )
67 64 22 32 66 36 fsum 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> sum_ m e. A ( ( k e. A |-> B ) ` m ) = ( seq 1 ( + , ( ( k e. A |-> B ) o. ( F o. f ) ) ) ` ( # ` C ) ) )
68 43 63 67 3eqtr4rd 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> sum_ m e. A ( ( k e. A |-> B ) ` m ) = sum_ m e. C ( ( n e. C |-> D ) ` m ) )
69 sumfc 
 |-  sum_ m e. A ( ( k e. A |-> B ) ` m ) = sum_ k e. A B
70 sumfc 
 |-  sum_ m e. C ( ( n e. C |-> D ) ` m ) = sum_ n e. C D
71 68 69 70 3eqtr3g 
 |-  ( ( ph /\ ( ( # ` C ) e. NN /\ f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) -> sum_ k e. A B = sum_ n e. C D )
72 71 expr 
 |-  ( ( ph /\ ( # ` C ) e. NN ) -> ( f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> sum_ k e. A B = sum_ n e. C D ) )
73 72 exlimdv 
 |-  ( ( ph /\ ( # ` C ) e. NN ) -> ( E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C -> sum_ k e. A B = sum_ n e. C D ) )
74 73 expimpd 
 |-  ( ph -> ( ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) -> sum_ k e. A B = sum_ n e. C D ) )
75 fz1f1o 
 |-  ( C e. Fin -> ( C = (/) \/ ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) )
76 2 75 syl 
 |-  ( ph -> ( C = (/) \/ ( ( # ` C ) e. NN /\ E. f f : ( 1 ... ( # ` C ) ) -1-1-onto-> C ) ) )
77 20 74 76 mpjaod 
 |-  ( ph -> sum_ k e. A B = sum_ n e. C D )