# Metamath Proof Explorer

## Theorem fsumf1of

Description: Re-index a finite sum using a bijection. Same as fsumf1o , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fsumf1of.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
fsumf1of.2 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
fsumf1of.3 ${⊢}{k}={G}\to {B}={D}$
fsumf1of.4 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
fsumf1of.5 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
fsumf1of.6 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
fsumf1of.7 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
Assertion fsumf1of ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$

### Proof

Step Hyp Ref Expression
1 fsumf1of.1 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
2 fsumf1of.2 ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{\phi }$
3 fsumf1of.3 ${⊢}{k}={G}\to {B}={D}$
4 fsumf1of.4 ${⊢}{\phi }\to {C}\in \mathrm{Fin}$
5 fsumf1of.5 ${⊢}{\phi }\to {F}:{C}\underset{1-1 onto}{⟶}{A}$
6 fsumf1of.6 ${⊢}\left({\phi }\wedge {n}\in {C}\right)\to {F}\left({n}\right)={G}$
7 fsumf1of.7 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
8 csbeq1a
9 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{A}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{A}$
11 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{B}$
12 nfcsb1v
13 8 9 10 11 12 cbvsum
14 13 a1i
15 nfv
16 nfcv
17 12 16 nfeq
18 15 17 nfim
19 eqeq1
20 8 eqeq1d
21 19 20 imbi12d
22 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{k}$
23 nfcsb1v
24 22 23 nfeq
25 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{B}$
26 nfcsb1v
27 25 26 nfeq
28 24 27 nfim
29 csbeq1a
30 29 eqeq2d
31 csbeq1a
32 31 eqeq2d
33 30 32 imbi12d
34 28 33 3 chvarfv
35 18 21 34 chvarfv
36 nfv ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}{j}\in {C}$
37 2 36 nfan ${⊢}Ⅎ{n}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {j}\in {C}\right)$
38 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{F}\left({j}\right)$
39 38 23 nfeq
40 37 39 nfim
41 eleq1w ${⊢}{n}={j}\to \left({n}\in {C}↔{j}\in {C}\right)$
42 41 anbi2d ${⊢}{n}={j}\to \left(\left({\phi }\wedge {n}\in {C}\right)↔\left({\phi }\wedge {j}\in {C}\right)\right)$
43 fveq2 ${⊢}{n}={j}\to {F}\left({n}\right)={F}\left({j}\right)$
44 43 29 eqeq12d
45 42 44 imbi12d
46 40 45 6 chvarfv
47 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{i}\in {A}$
48 1 47 nfan ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {i}\in {A}\right)$
49 12 nfel1
50 48 49 nfim
51 eleq1w ${⊢}{k}={i}\to \left({k}\in {A}↔{i}\in {A}\right)$
52 51 anbi2d ${⊢}{k}={i}\to \left(\left({\phi }\wedge {k}\in {A}\right)↔\left({\phi }\wedge {i}\in {A}\right)\right)$
53 8 eleq1d
54 52 53 imbi12d
55 50 54 7 chvarfv
56 35 4 5 46 55 fsumf1o
57 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{C}$
58 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{C}$
59 nfcv ${⊢}\underset{_}{Ⅎ}{j}\phantom{\rule{.4em}{0ex}}{D}$
60 31 57 58 59 26 cbvsum
61 60 eqcomi
62 61 a1i
63 14 56 62 3eqtrd ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=\sum _{{n}\in {C}}{D}$