fsumf1o

Description: Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014)

	Ref	Expression
Hypotheses	fsumf1o.1	$⊢ k = G \to B = D$
	fsumf1o.2	$⊢ φ \to C \in Fin$
	fsumf1o.3	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	fsumf1o.4	$⊢ (φ \land n \in C) \to F (n) = G$
	fsumf1o.5	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	fsumf1o	$⊢ φ \to \sum_{k \in A} B = \sum_{n \in C} D$

Proof

Step	Hyp	Ref	Expression
1		fsumf1o.1	$⊢ k = G \to B = D$
2		fsumf1o.2	$⊢ φ \to C \in Fin$
3		fsumf1o.3	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
4		fsumf1o.4	$⊢ (φ \land n \in C) \to F (n) = G$
5		fsumf1o.5	$⊢ (φ \land k \in A) \to B \in ℂ$
6		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
7		f1oeq2	$⊢ C = \emptyset \to (F : C \underset{1-1 onto}{⟶} A \leftrightarrow F : \emptyset \underset{1-1 onto}{⟶} A)$
8	3 7	syl5ibcom	$⊢ φ \to (C = \emptyset \to F : \emptyset \underset{1-1 onto}{⟶} A)$
9	8	imp	$⊢ (φ \land C = \emptyset) \to F : \emptyset \underset{1-1 onto}{⟶} A$
10		f1ofo	$⊢ F : \emptyset \underset{1-1 onto}{⟶} A \to F : \emptyset \underset{onto}{⟶} A$
11		fo00	$⊢ F : \emptyset \underset{onto}{⟶} A \leftrightarrow (F = \emptyset \land A = \emptyset)$
12	11	simprbi	$⊢ F : \emptyset \underset{onto}{⟶} A \to A = \emptyset$
13	9 10 12	3syl	$⊢ (φ \land C = \emptyset) \to A = \emptyset$
14	13	sumeq1d	$⊢ (φ \land C = \emptyset) \to \sum_{k \in A} B = \sum_{k \in \emptyset} B$
15		simpr	$⊢ (φ \land C = \emptyset) \to C = \emptyset$
16	15	sumeq1d	$⊢ (φ \land C = \emptyset) \to \sum_{n \in C} D = \sum_{n \in \emptyset} D$
17		sum0	$⊢ \sum_{n \in \emptyset} D = 0$
18	16 17	eqtrdi	$⊢ (φ \land C = \emptyset) \to \sum_{n \in C} D = 0$
19	6 14 18	3eqtr4a	$⊢ (φ \land C = \emptyset) \to \sum_{k \in A} B = \sum_{n \in C} D$
20	19	ex	$⊢ φ \to (C = \emptyset \to \sum_{k \in A} B = \sum_{n \in C} D)$
21		2fveq3	$⊢ m = f (n) \to (k \in A ⟼ B) (F (m)) = (k \in A ⟼ B) (F (f (n)))$
22		simprl	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \|C\| \in ℕ$
23		simprr	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C$
24		f1of	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C ⟶ A$
25	3 24	syl	$⊢ φ \to F : C ⟶ A$
26	25	ffvelrnda	$⊢ (φ \land m \in C) \to F (m) \in A$
27	5	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
28	27	ffvelrnda	$⊢ (φ \land F (m) \in A) \to (k \in A ⟼ B) (F (m)) \in ℂ$
29	26 28	syldan	$⊢ (φ \land m \in C) \to (k \in A ⟼ B) (F (m)) \in ℂ$
30	29	adantlr	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in C) \to (k \in A ⟼ B) (F (m)) \in ℂ$
31		f1oco	$⊢ (F : C \underset{1-1 onto}{⟶} A \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A$
32	3 23 31	syl2an2r	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A$
33		f1of	$⊢ (F \circ f) : (1 \dots \|C\|) \underset{1-1 onto}{⟶} A \to (F \circ f) : (1 \dots \|C\|) ⟶ A$
34	32 33	syl	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (F \circ f) : (1 \dots \|C\|) ⟶ A$
35		fvco3	$⊢ ((F \circ f) : (1 \dots \|C\|) ⟶ A \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) ((F \circ f) (n))$
36	34 35	sylan	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) ((F \circ f) (n))$
37		f1of	$⊢ f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to f : (1 \dots \|C\|) ⟶ C$
38	37	ad2antll	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to f : (1 \dots \|C\|) ⟶ C$
39		fvco3	$⊢ (f : (1 \dots \|C\|) ⟶ C \land n \in (1 \dots \|C\|)) \to (F \circ f) (n) = F (f (n))$
40	38 39	sylan	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to (F \circ f) (n) = F (f (n))$
41	40	fveq2d	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to (k \in A ⟼ B) ((F \circ f) (n)) = (k \in A ⟼ B) (F (f (n)))$
42	36 41	eqtrd	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land n \in (1 \dots \|C\|)) \to ((k \in A ⟼ B) \circ (F \circ f)) (n) = (k \in A ⟼ B) (F (f (n)))$
43	21 22 23 30 42	fsum	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \sum_{m \in C} (k \in A ⟼ B) (F (m)) = seq 1 (+ ((k \in A ⟼ B) \circ (F \circ f))) (\|C\|)$
44	25	ffvelrnda	$⊢ (φ \land n \in C) \to F (n) \in A$
45	4 44	eqeltrrd	$⊢ (φ \land n \in C) \to G \in A$
46		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
47	1 46	fvmpti	$⊢ G \in A \to (k \in A ⟼ B) (G) = I (D)$
48	45 47	syl	$⊢ (φ \land n \in C) \to (k \in A ⟼ B) (G) = I (D)$
49	4	fveq2d	$⊢ (φ \land n \in C) \to (k \in A ⟼ B) (F (n)) = (k \in A ⟼ B) (G)$
50		eqid	$⊢ (n \in C ⟼ D) = (n \in C ⟼ D)$
51	50	fvmpt2i	$⊢ n \in C \to (n \in C ⟼ D) (n) = I (D)$
52	51	adantl	$⊢ (φ \land n \in C) \to (n \in C ⟼ D) (n) = I (D)$
53	48 49 52	3eqtr4rd	$⊢ (φ \land n \in C) \to (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n))$
54	53	ralrimiva	$⊢ φ \to \forall n \in C (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n))$
55		nffvmpt1	$⊢ \underline{Ⅎ} n (n \in C ⟼ D) (m)$
56	55	nfeq1	$⊢ Ⅎ n (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
57		fveq2	$⊢ n = m \to (n \in C ⟼ D) (n) = (n \in C ⟼ D) (m)$
58		2fveq3	$⊢ n = m \to (k \in A ⟼ B) (F (n)) = (k \in A ⟼ B) (F (m))$
59	57 58	eqeq12d	$⊢ n = m \to ((n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n)) \leftrightarrow (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m)))$
60	56 59	rspc	$⊢ m \in C \to (\forall n \in C (n \in C ⟼ D) (n) = (k \in A ⟼ B) (F (n)) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m)))$
61	54 60	mpan9	$⊢ (φ \land m \in C) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
62	61	adantlr	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in C) \to (n \in C ⟼ D) (m) = (k \in A ⟼ B) (F (m))$
63	62	sumeq2dv	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \sum_{m \in C} (n \in C ⟼ D) (m) = \sum_{m \in C} (k \in A ⟼ B) (F (m))$
64		fveq2	$⊢ m = (F \circ f) (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) ((F \circ f) (n))$
65	27	adantr	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to (k \in A ⟼ B) : A ⟶ ℂ$
66	65	ffvelrnda	$⊢ ((φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
67	64 22 32 66 36	fsum	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \sum_{m \in A} (k \in A ⟼ B) (m) = seq 1 (+ ((k \in A ⟼ B) \circ (F \circ f))) (\|C\|)$
68	43 63 67	3eqtr4rd	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{m \in C} (n \in C ⟼ D) (m)$
69		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{k \in A} B$
70		sumfc	$⊢ \sum_{m \in C} (n \in C ⟼ D) (m) = \sum_{n \in C} D$
71	68 69 70	3eqtr3g	$⊢ (φ \land (\|C\| \in ℕ \land f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C)) \to \sum_{k \in A} B = \sum_{n \in C} D$
72	71	expr	$⊢ (φ \land \|C\| \in ℕ) \to (f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to \sum_{k \in A} B = \sum_{n \in C} D)$
73	72	exlimdv	$⊢ (φ \land \|C\| \in ℕ) \to (\exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C \to \sum_{k \in A} B = \sum_{n \in C} D)$
74	73	expimpd	$⊢ φ \to ((\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C) \to \sum_{k \in A} B = \sum_{n \in C} D)$
75		fz1f1o	$⊢ C \in Fin \to (C = \emptyset \lor (\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C))$
76	2 75	syl	$⊢ φ \to (C = \emptyset \lor (\|C\| \in ℕ \land \exists f f : (1 \dots \|C\|) \underset{1-1 onto}{⟶} C))$
77	20 74 76	mpjaod	$⊢ φ \to \sum_{k \in A} B = \sum_{n \in C} D$

Metamath Proof Explorer

Theorem fsumf1o

Proof