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	⊢ Ⅎ 𝑘 𝜑
	fsumf1of.2	⊢ Ⅎ 𝑛 𝜑
	fsumf1of.3	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
	fsumf1of.4	⊢ ( 𝜑 → 𝐶 ∈ Fin )
	fsumf1of.5	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
	fsumf1of.6	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
	fsumf1of.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fsumf1of	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fsumf1of.1	⊢ Ⅎ 𝑘 𝜑
2		fsumf1of.2	⊢ Ⅎ 𝑛 𝜑
3		fsumf1of.3	⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
4		fsumf1of.4	⊢ ( 𝜑 → 𝐶 ∈ Fin )
5		fsumf1of.5	⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
6		fsumf1of.6	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
7		fsumf1of.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8		csbeq1a	⊢ ( 𝑘 = 𝑖 → 𝐵 = ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
9		nfcv	⊢ Ⅎ 𝑖 𝐴
10		nfcv	⊢ Ⅎ 𝑘 𝐴
11		nfcv	⊢ Ⅎ 𝑖 𝐵
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	⊢ Ⅎ 𝑛 𝑘
23		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑗 / 𝑛 ⦌ 𝐺
24	22 23	nfeq	⊢ Ⅎ 𝑛 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺
25		nfcv	⊢ Ⅎ 𝑛 𝐵
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	⊢ Ⅎ 𝑛 𝑗 ∈ 𝐶
37	2 36	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑗 ∈ 𝐶 )
38		nfcv	⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑗 )
39	38 23	nfeq	⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺
40	37 39	nfim	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 )
41		eleq1w	⊢ ( 𝑛 = 𝑗 → ( 𝑛 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶 ) )
42	41	anbi2d	⊢ ( 𝑛 = 𝑗 → ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) ) )
43		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
44	43 29	eqeq12d	⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) = 𝐺 ↔ ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) )
45	42 44	imbi12d	⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) ) )
46	40 45 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 )
47		nfv	⊢ Ⅎ 𝑘 𝑖 ∈ 𝐴
48	1 47	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝐴 )
49	12	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ
50	48 49	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
51		eleq1w	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
52	51	anbi2d	⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) )
53	8	eleq1d	⊢ ( 𝑘 = 𝑖 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
54	52 53	imbi12d	⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
55	50 54 7	chvarfv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
56	35 4 5 46 55	fsumf1o	⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
57		nfcv	⊢ Ⅎ 𝑗 𝐶
58		nfcv	⊢ Ⅎ 𝑛 𝐶
59		nfcv	⊢ Ⅎ 𝑗 𝐷
60	31 57 58 59 26	cbvsum	⊢ Σ 𝑛 ∈ 𝐶 𝐷 = Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷
61	60	eqcomi	⊢ Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 = Σ 𝑛 ∈ 𝐶 𝐷
62	61	a1i	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 = Σ 𝑛 ∈ 𝐶 𝐷 )
63	14 56 62	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )