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\phi$$
	fsumf1of.2	$$⊢Ⅎn\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\phi$$
2		fsumf1of.2	$$⊢Ⅎn\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	$$⊢k=i\to B=⦋i/k⦌B$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}iA$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}iB$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋i/k⦌B$$
13	8 9 10 11 12	cbvsum	$$⊢\sum _{k\in A}B=\sum _{i\in A}⦋i/k⦌B$$
14	13	a1i	$$⊢\phi \to \sum _{k\in A}B=\sum _{i\in A}⦋i/k⦌B$$
15		nfv	$$⊢Ⅎki=⦋j/n⦌G$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}k⦋j/n⦌D$$
17	12 16	nfeq	$$⊢Ⅎk⦋i/k⦌B=⦋j/n⦌D$$
18	15 17	nfim	$$⊢Ⅎk\left(i=⦋j/n⦌G\to ⦋i/k⦌B=⦋j/n⦌D\right)$$
19		eqeq1	$$⊢k=i\to \left(k=⦋j/n⦌G\leftrightarrow i=⦋j/n⦌G\right)$$
20	8	eqeq1d	$$⊢k=i\to \left(B=⦋j/n⦌D\leftrightarrow ⦋i/k⦌B=⦋j/n⦌D\right)$$
21	19 20	imbi12d	$$⊢k=i\to \left(\left(k=⦋j/n⦌G\to B=⦋j/n⦌D\right)\leftrightarrow \left(i=⦋j/n⦌G\to ⦋i/k⦌B=⦋j/n⦌D\right)\right)$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}nk$$
23		nfcsb1v	$$⊢\underset{\_}{Ⅎ}n⦋j/n⦌G$$
24	22 23	nfeq	$$⊢Ⅎnk=⦋j/n⦌G$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}nB$$
26		nfcsb1v	$$⊢\underset{\_}{Ⅎ}n⦋j/n⦌D$$
27	25 26	nfeq	$$⊢ℲnB=⦋j/n⦌D$$
28	24 27	nfim	$$⊢Ⅎn\left(k=⦋j/n⦌G\to B=⦋j/n⦌D\right)$$
29		csbeq1a	$$⊢n=j\to G=⦋j/n⦌G$$
30	29	eqeq2d	$$⊢n=j\to \left(k=G\leftrightarrow k=⦋j/n⦌G\right)$$
31		csbeq1a	$$⊢n=j\to D=⦋j/n⦌D$$
32	31	eqeq2d	$$⊢n=j\to \left(B=D\leftrightarrow B=⦋j/n⦌D\right)$$
33	30 32	imbi12d	$$⊢n=j\to \left(\left(k=G\to B=D\right)\leftrightarrow \left(k=⦋j/n⦌G\to B=⦋j/n⦌D\right)\right)$$
34	28 33 3	chvarfv	$$⊢k=⦋j/n⦌G\to B=⦋j/n⦌D$$
35	18 21 34	chvarfv	$$⊢i=⦋j/n⦌G\to ⦋i/k⦌B=⦋j/n⦌D$$
36		nfv	$$⊢Ⅎnj\in C$$
37	2 36	nfan	$$⊢Ⅎn\left(\phi \wedge j\in C\right)$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}nF\left(j\right)$$
39	38 23	nfeq	$$⊢ℲnF\left(j\right)=⦋j/n⦌G$$
40	37 39	nfim	$$⊢Ⅎn\left(\left(\phi \wedge j\in C\right)\to F\left(j\right)=⦋j/n⦌G\right)$$
41		eleq1w	$$⊢n=j\to \left(n\in C\leftrightarrow j\in C\right)$$
42	41	anbi2d	$$⊢n=j\to \left(\left(\phi \wedge n\in C\right)\leftrightarrow \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	$$⊢n=j\to \left(F\left(n\right)=G\leftrightarrow F\left(j\right)=⦋j/n⦌G\right)$$
45	42 44	imbi12d	$$⊢n=j\to \left(\left(\left(\phi \wedge n\in C\right)\to F\left(n\right)=G\right)\leftrightarrow \left(\left(\phi \wedge j\in C\right)\to F\left(j\right)=⦋j/n⦌G\right)\right)$$
46	40 45 6	chvarfv	$$⊢\left(\phi \wedge j\in C\right)\to F\left(j\right)=⦋j/n⦌G$$
47		nfv	$$⊢Ⅎki\in A$$
48	1 47	nfan	$$⊢Ⅎk\left(\phi \wedge i\in A\right)$$
49	12	nfel1	$$⊢Ⅎk⦋i/k⦌B\in ℂ$$
50	48 49	nfim	$$⊢Ⅎk\left(\left(\phi \wedge i\in A\right)\to ⦋i/k⦌B\in ℂ\right)$$
51		eleq1w	$$⊢k=i\to \left(k\in A\leftrightarrow i\in A\right)$$
52	51	anbi2d	$$⊢k=i\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge i\in A\right)\right)$$
53	8	eleq1d	$$⊢k=i\to \left(B\in ℂ\leftrightarrow ⦋i/k⦌B\in ℂ\right)$$
54	52 53	imbi12d	$$⊢k=i\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge i\in A\right)\to ⦋i/k⦌B\in ℂ\right)\right)$$
55	50 54 7	chvarfv	$$⊢\left(\phi \wedge i\in A\right)\to ⦋i/k⦌B\in ℂ$$
56	35 4 5 46 55	fsumf1o	$$⊢\phi \to \sum _{i\in A}⦋i/k⦌B=\sum _{j\in C}⦋j/n⦌D$$
57		nfcv	$$⊢\underset{\_}{Ⅎ}jC$$
58		nfcv	$$⊢\underset{\_}{Ⅎ}nC$$
59		nfcv	$$⊢\underset{\_}{Ⅎ}jD$$
60	31 57 58 59 26	cbvsum	$$⊢\sum _{n\in C}D=\sum _{j\in C}⦋j/n⦌D$$
61	60	eqcomi	$$⊢\sum _{j\in C}⦋j/n⦌D=\sum _{n\in C}D$$
62	61	a1i	$$⊢\phi \to \sum _{j\in C}⦋j/n⦌D=\sum _{n\in C}D$$
63	14 56 62	3eqtrd	$$⊢\phi \to \sum _{k\in A}B=\sum _{n\in C}D$$