# 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}\to {B}={D}$
fsumf1o.2 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
fsumf1o.3 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
fsumf1o.4 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
fsumf1o.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
Assertion fsumf1o ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$

### Proof

Step Hyp Ref Expression
1 fsumf1o.1 ${⊢}{k}={G}\to {B}={D}$
2 fsumf1o.2 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
3 fsumf1o.3 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
4 fsumf1o.4 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
5 fsumf1o.5 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
6 sum0 ${⊢}\sum _{{k}\in \varnothing }{B}=0$
7 f1oeq2 ${⊢}{C}=\varnothing \to \left({F}:{C}\underset{1-1 onto}{⟶}{A}↔{F}:\varnothing \underset{1-1 onto}{⟶}{A}\right)$
8 3 7 syl5ibcom ${⊢}{\phi }\to \left({C}=\varnothing \to {F}:\varnothing \underset{1-1 onto}{⟶}{A}\right)$
9 8 imp ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {F}:\varnothing \underset{1-1 onto}{⟶}{A}$
10 f1ofo ${⊢}{F}:\varnothing \underset{1-1 onto}{⟶}{A}\to {F}:\varnothing \underset{onto}{⟶}{A}$
11 fo00 ${⊢}{F}:\varnothing \underset{onto}{⟶}{A}↔\left({F}=\varnothing \wedge {A}=\varnothing \right)$
12 11 simprbi ${⊢}{F}:\varnothing \underset{onto}{⟶}{A}\to {A}=\varnothing$
13 9 10 12 3syl ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {A}=\varnothing$
14 13 sumeq1d ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \sum _{{k}\in {A}}{B}=\sum _{{k}\in \varnothing }{B}$
15 simpr ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to {C}=\varnothing$
16 15 sumeq1d ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \sum _{{n}\in {C}}{D}=\sum _{{n}\in \varnothing }{D}$
17 sum0 ${⊢}\sum _{{n}\in \varnothing }{D}=0$
18 16 17 syl6eq ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \sum _{{n}\in {C}}{D}=0$
19 6 14 18 3eqtr4a ${⊢}\left({\phi }\wedge {C}=\varnothing \right)\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$
20 19 ex ${⊢}{\phi }\to \left({C}=\varnothing \to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}\right)$
21 2fveq3 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
22 simprl ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left|{C}\right|\in ℕ$
23 simprr ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}$
24 f1of ${⊢}{F}:{C}\underset{1-1 onto}{⟶}{A}\to {F}:{C}⟶{A}$
25 3 24 syl ${⊢}{\phi }\to {F}:{C}⟶{A}$
26 25 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to {F}\left({m}\right)\in {A}$
27 5 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
28 27 ffvelrnda ${⊢}\left({\phi }\wedge {F}\left({m}\right)\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
29 26 28 syldan ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
30 29 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\in ℂ$
31 f1oco ${⊢}\left({F}:{C}\underset{1-1 onto}{⟶}{A}\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}$
32 3 23 31 syl2an2r ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}$
33 f1of ${⊢}\left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{A}\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}$
34 32 33 syl ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}$
35 fvco3 ${⊢}\left(\left({F}\circ {f}\right):\left(1\dots \left|{C}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
36 34 35 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
37 f1of ${⊢}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to {f}:\left(1\dots \left|{C}\right|\right)⟶{C}$
38 37 ad2antll ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to {f}:\left(1\dots \left|{C}\right|\right)⟶{C}$
39 fvco3 ${⊢}\left({f}:\left(1\dots \left|{C}\right|\right)⟶{C}\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({F}\circ {f}\right)\left({n}\right)={F}\left({f}\left({n}\right)\right)$
40 38 39 sylan ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({F}\circ {f}\right)\left({n}\right)={F}\left({f}\left({n}\right)\right)$
41 40 fveq2d ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
42 36 41 eqtrd ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {n}\in \left(1\dots \left|{C}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({f}\left({n}\right)\right)\right)$
43 21 22 23 30 42 fsum ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \sum _{{m}\in {C}}\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\right)\left(\left|{C}\right|\right)$
44 25 ffvelrnda ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)\in {A}$
45 4 44 eqeltrrd ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {G}\in {A}$
46 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
47 1 46 fvmpti ${⊢}{G}\in {A}\to \left({k}\in {A}⟼{B}\right)\left({G}\right)=\mathrm{I}\left({D}\right)$
48 45 47 syl ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({G}\right)=\mathrm{I}\left({D}\right)$
49 4 fveq2d ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({G}\right)$
50 eqid ${⊢}\left({n}\in {C}⟼{D}\right)=\left({n}\in {C}⟼{D}\right)$
51 50 fvmpt2i ${⊢}{n}\in {C}\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\mathrm{I}\left({D}\right)$
52 51 adantl ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\mathrm{I}\left({D}\right)$
53 48 49 52 3eqtr4rd ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)$
54 53 ralrimiva ${⊢}{\phi }\to \forall {n}\in {C}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)$
55 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({m}\right)$
56 55 nfeq1 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
57 fveq2 ${⊢}{n}={m}\to \left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({n}\in {C}⟼{D}\right)\left({m}\right)$
58 2fveq3 ${⊢}{n}={m}\to \left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
59 57 58 eqeq12d ${⊢}{n}={m}\to \left(\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)↔\left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\right)$
60 56 59 rspc ${⊢}{m}\in {C}\to \left(\forall {n}\in {C}\phantom{\rule{.4em}{0ex}}\left({n}\in {C}⟼{D}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({n}\right)\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)\right)$
61 54 60 mpan9 ${⊢}\left({\phi }\wedge {m}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
62 61 adantlr ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {C}\right)\to \left({n}\in {C}⟼{D}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
63 62 sumeq2dv ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \sum _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\sum _{{m}\in {C}}\left({k}\in {A}⟼{B}\right)\left({F}\left({m}\right)\right)$
64 fveq2 ${⊢}{m}=\left({F}\circ {f}\right)\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left(\left({F}\circ {f}\right)\left({n}\right)\right)$
65 27 adantr ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \left({k}\in {A}⟼{B}\right):{A}⟶ℂ$
66 65 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)\in ℂ$
67 64 22 32 66 36 fsum ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ \left({F}\circ {f}\right)\right)\right)\left(\left|{C}\right|\right)$
68 43 63 67 3eqtr4rd ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\sum _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)$
69 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\sum _{{k}\in {A}}{B}$
70 sumfc ${⊢}\sum _{{m}\in {C}}\left({n}\in {C}⟼{D}\right)\left({m}\right)=\sum _{{n}\in {C}}{D}$
71 68 69 70 3eqtr3g ${⊢}\left({\phi }\wedge \left(\left|{C}\right|\in ℕ\wedge {f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$
72 71 expr ${⊢}\left({\phi }\wedge \left|{C}\right|\in ℕ\right)\to \left({f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}\right)$
73 72 exlimdv ${⊢}\left({\phi }\wedge \left|{C}\right|\in ℕ\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}\right)$
74 73 expimpd ${⊢}{\phi }\to \left(\left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}\right)$
75 fz1f1o ${⊢}{C}\in \mathrm{Fin}\to \left({C}=\varnothing \vee \left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)$
76 2 75 syl ${⊢}{\phi }\to \left({C}=\varnothing \vee \left(\left|{C}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{C}\right|\right)\underset{1-1 onto}{⟶}{C}\right)\right)$
77 20 74 76 mpjaod ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$