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 φ$
	fsumf1of.2	$⊢ Ⅎ n φ$
	fsumf1of.3	$⊢ k = G \to B = D$
	fsumf1of.4	$⊢ φ \to C \in Fin$
	fsumf1of.5	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	fsumf1of.6	$⊢ (φ \land n \in C) \to F (n) = G$
	fsumf1of.7	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fsumf1of	$⊢ φ \to \sum_{k \in A} B = \sum_{n \in C} D$

Proof

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

Metamath Proof Explorer

Theorem fsumf1of

Proof