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 φ C Fin
fsumf1o.3 φ F : C 1-1 onto A
fsumf1o.4 φ n C F n = G
fsumf1o.5 φ k A B
Assertion fsumf1o φ k A B = n C D

Proof

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