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		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
11	8 9 10	cbvsum	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵
12	11	a1i	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 )
13		nfv	⊢ Ⅎ 𝑘 𝑖 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺
14		nfcv	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑛 ⦌ 𝐷
15	10 14	nfeq	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷
16	13 15	nfim	⊢ Ⅎ 𝑘 ( 𝑖 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
17		eqeq1	⊢ ( 𝑘 = 𝑖 → ( 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ↔ 𝑖 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) )
18	8	eqeq1d	⊢ ( 𝑘 = 𝑖 → ( 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ) )
19	17 18	imbi12d	⊢ ( 𝑘 = 𝑖 → ( ( 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ) ↔ ( 𝑖 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ) ) )
20		nfcv	⊢ Ⅎ 𝑛 𝑘
21		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑗 / 𝑛 ⦌ 𝐺
22	20 21	nfeq	⊢ Ⅎ 𝑛 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺
23		nfcv	⊢ Ⅎ 𝑛 𝐵
24		nfcsb1v	⊢ Ⅎ 𝑛 ⦋ 𝑗 / 𝑛 ⦌ 𝐷
25	23 24	nfeq	⊢ Ⅎ 𝑛 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷
26	22 25	nfim	⊢ Ⅎ 𝑛 ( 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
27		csbeq1a	⊢ ( 𝑛 = 𝑗 → 𝐺 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 )
28	27	eqeq2d	⊢ ( 𝑛 = 𝑗 → ( 𝑘 = 𝐺 ↔ 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) )
29		csbeq1a	⊢ ( 𝑛 = 𝑗 → 𝐷 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
30	29	eqeq2d	⊢ ( 𝑛 = 𝑗 → ( 𝐵 = 𝐷 ↔ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ) )
31	28 30	imbi12d	⊢ ( 𝑛 = 𝑗 → ( ( 𝑘 = 𝐺 → 𝐵 = 𝐷 ) ↔ ( 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 ) ) )
32	26 31 3	chvarfv	⊢ ( 𝑘 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
33	16 19 32	chvarfv	⊢ ( 𝑖 = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
34		nfv	⊢ Ⅎ 𝑛 𝑗 ∈ 𝐶
35	2 34	nfan	⊢ Ⅎ 𝑛 ( 𝜑 ∧ 𝑗 ∈ 𝐶 )
36		nfcv	⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑗 )
37	36 21	nfeq	⊢ Ⅎ 𝑛 ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺
38	35 37	nfim	⊢ Ⅎ 𝑛 ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 )
39		eleq1w	⊢ ( 𝑛 = 𝑗 → ( 𝑛 ∈ 𝐶 ↔ 𝑗 ∈ 𝐶 ) )
40	39	anbi2d	⊢ ( 𝑛 = 𝑗 → ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) ) )
41		fveq2	⊢ ( 𝑛 = 𝑗 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑗 ) )
42	41 27	eqeq12d	⊢ ( 𝑛 = 𝑗 → ( ( 𝐹 ‘ 𝑛 ) = 𝐺 ↔ ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) )
43	40 42	imbi12d	⊢ ( 𝑛 = 𝑗 → ( ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 ) ) )
44	38 43 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑗 ) = ⦋ 𝑗 / 𝑛 ⦌ 𝐺 )
45		nfv	⊢ Ⅎ 𝑘 𝑖 ∈ 𝐴
46	1 45	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑖 ∈ 𝐴 )
47	10	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ
48	46 47	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
49		eleq1w	⊢ ( 𝑘 = 𝑖 → ( 𝑘 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 ) )
50	49	anbi2d	⊢ ( 𝑘 = 𝑖 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ) )
51	8	eleq1d	⊢ ( 𝑘 = 𝑖 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) )
52	50 51	imbi12d	⊢ ( 𝑘 = 𝑖 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ ) ) )
53	48 52 7	chvarfv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑘 ⦌ 𝐵 ∈ ℂ )
54	33 4 5 44 53	fsumf1o	⊢ ( 𝜑 → Σ 𝑖 ∈ 𝐴 ⦋ 𝑖 / 𝑘 ⦌ 𝐵 = Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 )
55		nfcv	⊢ Ⅎ 𝑗 𝐷
56	29 55 24	cbvsum	⊢ Σ 𝑛 ∈ 𝐶 𝐷 = Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷
57	56	eqcomi	⊢ Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 = Σ 𝑛 ∈ 𝐶 𝐷
58	57	a1i	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑛 ⦌ 𝐷 = Σ 𝑛 ∈ 𝐶 𝐷 )
59	12 54 58	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )