fsumss

Description: Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014)

	Ref	Expression
Hypotheses	sumss.1	$⊢ φ \to A \subseteq B$
	sumss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
	sumss.3	$⊢ (φ \land k \in (B ∖ A)) \to C = 0$
	fsumss.4	$⊢ φ \to B \in Fin$
Assertion	fsumss	$⊢ φ \to \sum_{k \in A} C = \sum_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		sumss.1	$⊢ φ \to A \subseteq B$
2		sumss.2	$⊢ (φ \land k \in A) \to C \in ℂ$
3		sumss.3	$⊢ (φ \land k \in (B ∖ A)) \to C = 0$
4		fsumss.4	$⊢ φ \to B \in Fin$
5	1	adantr	$⊢ (φ \land B = \emptyset) \to A \subseteq B$
6	2	adantlr	$⊢ ((φ \land B = \emptyset) \land k \in A) \to C \in ℂ$
7	3	adantlr	$⊢ ((φ \land B = \emptyset) \land k \in (B ∖ A)) \to C = 0$
8		simpr	$⊢ (φ \land B = \emptyset) \to B = \emptyset$
9		0ss	$⊢ \emptyset \subseteq ℤ_{\geq 0}$
10	8 9	eqsstrdi	$⊢ (φ \land B = \emptyset) \to B \subseteq ℤ_{\geq 0}$
11	5 6 7 10	sumss	$⊢ (φ \land B = \emptyset) \to \sum_{k \in A} C = \sum_{k \in B} C$
12	11	ex	$⊢ φ \to (B = \emptyset \to \sum_{k \in A} C = \sum_{k \in B} C)$
13		cnvimass	$⊢ f^{-1} [A] \subseteq dom f$
14		simprr	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B$
15		f1of	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) ⟶ B$
16	14 15	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) ⟶ B$
17	13 16	fssdm	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f^{-1} [A] \subseteq (1 \dots \|B\|)$
18	16	ffnd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f Fn (1 \dots \|B\|)$
19		elpreima	$⊢ f Fn (1 \dots \|B\|) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
20	18 19	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
21	16	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in (1 \dots \|B\|)) \to f (n) \in B$
22	21	ex	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in (1 \dots \|B\|) \to f (n) \in B)$
23	22	adantrd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ((n \in (1 \dots \|B\|) \land f (n) \in A) \to f (n) \in B)$
24	20 23	sylbid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (n \in f^{-1} [A] \to f (n) \in B)$
25	24	imp	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to f (n) \in B$
26	2	ex	$⊢ φ \to (k \in A \to C \in ℂ)$
27	26	adantr	$⊢ (φ \land k \in B) \to (k \in A \to C \in ℂ)$
28		eldif	$⊢ k \in (B ∖ A) \leftrightarrow (k \in B \land \neg k \in A)$
29		0cn	$⊢ 0 \in ℂ$
30	3 29	eqeltrdi	$⊢ (φ \land k \in (B ∖ A)) \to C \in ℂ$
31	28 30	sylan2br	$⊢ (φ \land (k \in B \land \neg k \in A)) \to C \in ℂ$
32	31	expr	$⊢ (φ \land k \in B) \to (\neg k \in A \to C \in ℂ)$
33	27 32	pm2.61d	$⊢ (φ \land k \in B) \to C \in ℂ$
34	33	fmpttd	$⊢ φ \to (k \in B ⟼ C) : B ⟶ ℂ$
35	34	adantr	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (k \in B ⟼ C) : B ⟶ ℂ$
36	35	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land f (n) \in B) \to (k \in B ⟼ C) (f (n)) \in ℂ$
37	25 36	syldan	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to (k \in B ⟼ C) (f (n)) \in ℂ$
38		eldifi	$⊢ n \in ((1 \dots \|B\|) ∖ f^{-1} [A]) \to n \in (1 \dots \|B\|)$
39	38 21	sylan2	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to f (n) \in B$
40		eldifn	$⊢ n \in ((1 \dots \|B\|) ∖ f^{-1} [A]) \to \neg n \in f^{-1} [A]$
41	40	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to \neg n \in f^{-1} [A]$
42	38	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to n \in (1 \dots \|B\|)$
43	20	adantr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (n \in f^{-1} [A] \leftrightarrow (n \in (1 \dots \|B\|) \land f (n) \in A))$
44	42 43	mpbirand	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (n \in f^{-1} [A] \leftrightarrow f (n) \in A)$
45	41 44	mtbid	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to \neg f (n) \in A$
46	39 45	eldifd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to f (n) \in (B ∖ A)$
47		difss	$⊢ B ∖ A \subseteq B$
48		resmpt	$⊢ B ∖ A \subseteq B \to {(k \in B ⟼ C) ↾}_{(B ∖ A)} = (k \in (B ∖ A) ⟼ C)$
49	47 48	ax-mp	$⊢ {(k \in B ⟼ C) ↾}_{(B ∖ A)} = (k \in (B ∖ A) ⟼ C)$
50	49	fveq1i	$⊢ ({(k \in B ⟼ C) ↾}_{(B ∖ A)}) (f (n)) = (k \in (B ∖ A) ⟼ C) (f (n))$
51		fvres	$⊢ f (n) \in (B ∖ A) \to ({(k \in B ⟼ C) ↾}_{(B ∖ A)}) (f (n)) = (k \in B ⟼ C) (f (n))$
52	50 51	syl5eqr	$⊢ f (n) \in (B ∖ A) \to (k \in (B ∖ A) ⟼ C) (f (n)) = (k \in B ⟼ C) (f (n))$
53	46 52	syl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) = (k \in B ⟼ C) (f (n))$
54		c0ex	$⊢ 0 \in V$
55	54	elsn2	$⊢ C \in \{0\} \leftrightarrow C = 0$
56	3 55	sylibr	$⊢ (φ \land k \in (B ∖ A)) \to C \in \{0\}$
57	56	fmpttd	$⊢ φ \to (k \in (B ∖ A) ⟼ C) : B ∖ A ⟶ \{0\}$
58	57	ad2antrr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) : B ∖ A ⟶ \{0\}$
59	58 46	ffvelrnd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) \in \{0\}$
60		elsni	$⊢ (k \in (B ∖ A) ⟼ C) (f (n)) \in \{0\} \to (k \in (B ∖ A) ⟼ C) (f (n)) = 0$
61	59 60	syl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in (B ∖ A) ⟼ C) (f (n)) = 0$
62	53 61	eqtr3d	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in ((1 \dots \|B\|) ∖ f^{-1} [A])) \to (k \in B ⟼ C) (f (n)) = 0$
63		fzssuz	$⊢ (1 \dots \|B\|) \subseteq ℤ_{\geq 1}$
64	63	a1i	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (1 \dots \|B\|) \subseteq ℤ_{\geq 1}$
65	17 37 62 64	sumss	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n)) = \sum_{n = 1}^{\|B\|} (k \in B ⟼ C) (f (n))$
66	1	ad2antrr	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to A \subseteq B$
67	66	resmptd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to {(k \in B ⟼ C) ↾}_{A} = (k \in A ⟼ C)$
68	67	fveq1d	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to ({(k \in B ⟼ C) ↾}_{A}) (m) = (k \in A ⟼ C) (m)$
69		fvres	$⊢ m \in A \to ({(k \in B ⟼ C) ↾}_{A}) (m) = (k \in B ⟼ C) (m)$
70	69	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to ({(k \in B ⟼ C) ↾}_{A}) (m) = (k \in B ⟼ C) (m)$
71	68 70	eqtr3d	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to (k \in A ⟼ C) (m) = (k \in B ⟼ C) (m)$
72	71	sumeq2dv	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{m \in A} (k \in B ⟼ C) (m)$
73		fveq2	$⊢ m = f (n) \to (k \in B ⟼ C) (m) = (k \in B ⟼ C) (f (n))$
74		fzfid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (1 \dots \|B\|) \in Fin$
75	74 16	fisuppfi	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f^{-1} [A] \in Fin$
76		f1of1	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) \underset{1-1}{⟶} B$
77	14 76	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{1-1}{⟶} B$
78		f1ores	$⊢ (f : (1 \dots \|B\|) \underset{1-1}{⟶} B \land f^{-1} [A] \subseteq (1 \dots \|B\|)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]]$
79	77 17 78	syl2anc	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]]$
80		f1ofo	$⊢ f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to f : (1 \dots \|B\|) \underset{onto}{⟶} B$
81	14 80	syl	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f : (1 \dots \|B\|) \underset{onto}{⟶} B$
82	1	adantr	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to A \subseteq B$
83		foimacnv	$⊢ (f : (1 \dots \|B\|) \underset{onto}{⟶} B \land A \subseteq B) \to f [f^{-1} [A]] = A$
84	81 82 83	syl2anc	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to f [f^{-1} [A]] = A$
85	84	f1oeq3d	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to (({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} f [f^{-1} [A]] \leftrightarrow ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A)$
86	79 85	mpbid	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to ({f ↾}_{f^{-1} [A]}) : f^{-1} [A] \underset{1-1 onto}{⟶} A$
87		fvres	$⊢ n \in f^{-1} [A] \to ({f ↾}_{f^{-1} [A]}) (n) = f (n)$
88	87	adantl	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in f^{-1} [A]) \to ({f ↾}_{f^{-1} [A]}) (n) = f (n)$
89	82	sselda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to m \in B$
90	35	ffvelrnda	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in B) \to (k \in B ⟼ C) (m) \in ℂ$
91	89 90	syldan	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land m \in A) \to (k \in B ⟼ C) (m) \in ℂ$
92	73 75 86 88 91	fsumf1o	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{m \in A} (k \in B ⟼ C) (m) = \sum_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n))$
93	72 92	eqtrd	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{n \in f^{-1} [A]} (k \in B ⟼ C) (f (n))$
94		eqidd	$⊢ ((φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \land n \in (1 \dots \|B\|)) \to f (n) = f (n)$
95	73 74 14 94 90	fsumf1o	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{m \in B} (k \in B ⟼ C) (m) = \sum_{n = 1}^{\|B\|} (k \in B ⟼ C) (f (n))$
96	65 93 95	3eqtr4d	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{m \in B} (k \in B ⟼ C) (m)$
97		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{k \in A} C$
98		sumfc	$⊢ \sum_{m \in B} (k \in B ⟼ C) (m) = \sum_{k \in B} C$
99	96 97 98	3eqtr3g	$⊢ (φ \land (\|B\| \in ℕ \land f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B)) \to \sum_{k \in A} C = \sum_{k \in B} C$
100	99	expr	$⊢ (φ \land \|B\| \in ℕ) \to (f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to \sum_{k \in A} C = \sum_{k \in B} C)$
101	100	exlimdv	$⊢ (φ \land \|B\| \in ℕ) \to (\exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B \to \sum_{k \in A} C = \sum_{k \in B} C)$
102	101	expimpd	$⊢ φ \to ((\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B) \to \sum_{k \in A} C = \sum_{k \in B} C)$
103		fz1f1o	$⊢ B \in Fin \to (B = \emptyset \lor (\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B))$
104	4 103	syl	$⊢ φ \to (B = \emptyset \lor (\|B\| \in ℕ \land \exists f f : (1 \dots \|B\|) \underset{1-1 onto}{⟶} B))$
105	12 102 104	mpjaod	$⊢ φ \to \sum_{k \in A} C = \sum_{k \in B} C$

Metamath Proof Explorer

Theorem fsumss

Proof