sumss

Description: Change the index set to a subset in an upper integer 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$
	sumss.4	$⊢ φ \to B \subseteq ℤ_{\geq M}$
Assertion	sumss	$⊢ φ \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		sumss.4	$⊢ φ \to B \subseteq ℤ_{\geq M}$
5		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
6		simpr	$⊢ (φ \land M \in ℤ) \to M \in ℤ$
7	1 4	sstrd	$⊢ φ \to A \subseteq ℤ_{\geq M}$
8	7	adantr	$⊢ (φ \land M \in ℤ) \to A \subseteq ℤ_{\geq M}$
9		nfcv	$⊢ \underline{Ⅎ} k m$
10		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m)$
11		nfv	$⊢ Ⅎ k m \in A$
12		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C) (m)$
13		nfcv	$⊢ \underline{Ⅎ} k 0$
14	11 12 13	nfif	$⊢ \underline{Ⅎ} k if (m \in A, (k \in A ⟼ C) (m), 0)$
15	10 14	nfeq	$⊢ Ⅎ k (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in A, (k \in A ⟼ C) (m), 0)$
16		fveq2	$⊢ k = m \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m)$
17		eleq1w	$⊢ k = m \to (k \in A \leftrightarrow m \in A)$
18		fveq2	$⊢ k = m \to (k \in A ⟼ C) (k) = (k \in A ⟼ C) (m)$
19	17 18	ifbieq1d	$⊢ k = m \to if (k \in A, (k \in A ⟼ C) (k), 0) = if (m \in A, (k \in A ⟼ C) (m), 0)$
20	16 19	eqeq12d	$⊢ k = m \to ((k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in A, (k \in A ⟼ C) (k), 0) \leftrightarrow (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in A, (k \in A ⟼ C) (m), 0))$
21		eqid	$⊢ (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) = (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0))$
22	21	fvmpt2i	$⊢ k \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = I (if (k \in A, C, 0))$
23		iftrue	$⊢ k \in A \to if (k \in A, C, 0) = C$
24	23	fveq2d	$⊢ k \in A \to I (if (k \in A, C, 0)) = I (C)$
25	22 24	sylan9eq	$⊢ (k \in ℤ_{\geq M} \land k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = I (C)$
26		iftrue	$⊢ k \in A \to if (k \in A, (k \in A ⟼ C) (k), 0) = (k \in A ⟼ C) (k)$
27		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
28	27	fvmpt2i	$⊢ k \in A \to (k \in A ⟼ C) (k) = I (C)$
29	26 28	eqtrd	$⊢ k \in A \to if (k \in A, (k \in A ⟼ C) (k), 0) = I (C)$
30	29	adantl	$⊢ (k \in ℤ_{\geq M} \land k \in A) \to if (k \in A, (k \in A ⟼ C) (k), 0) = I (C)$
31	25 30	eqtr4d	$⊢ (k \in ℤ_{\geq M} \land k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in A, (k \in A ⟼ C) (k), 0)$
32		iffalse	$⊢ \neg k \in A \to if (k \in A, C, 0) = 0$
33	32	fveq2d	$⊢ \neg k \in A \to I (if (k \in A, C, 0)) = I (0)$
34		0z	$⊢ 0 \in ℤ$
35		fvi	$⊢ 0 \in ℤ \to I (0) = 0$
36	34 35	ax-mp	$⊢ I (0) = 0$
37	33 36	eqtrdi	$⊢ \neg k \in A \to I (if (k \in A, C, 0)) = 0$
38	22 37	sylan9eq	$⊢ (k \in ℤ_{\geq M} \land \neg k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = 0$
39		iffalse	$⊢ \neg k \in A \to if (k \in A, (k \in A ⟼ C) (k), 0) = 0$
40	39	adantl	$⊢ (k \in ℤ_{\geq M} \land \neg k \in A) \to if (k \in A, (k \in A ⟼ C) (k), 0) = 0$
41	38 40	eqtr4d	$⊢ (k \in ℤ_{\geq M} \land \neg k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in A, (k \in A ⟼ C) (k), 0)$
42	31 41	pm2.61dan	$⊢ k \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in A, (k \in A ⟼ C) (k), 0)$
43	9 15 20 42	vtoclgaf	$⊢ m \in ℤ_{\geq M} \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in A, (k \in A ⟼ C) (m), 0)$
44	43	adantl	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in A, (k \in A ⟼ C) (m), 0)$
45	2	fmpttd	$⊢ φ \to (k \in A ⟼ C) : A ⟶ ℂ$
46	45	adantr	$⊢ (φ \land M \in ℤ) \to (k \in A ⟼ C) : A ⟶ ℂ$
47	46	ffvelcdmda	$⊢ ((φ \land M \in ℤ) \land m \in A) \to (k \in A ⟼ C) (m) \in ℂ$
48	5 6 8 44 47	zsum	$⊢ (φ \land M \in ℤ) \to \sum_{m \in A} (k \in A ⟼ C) (m) = ⇝ (seq M (+ (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0))))$
49	4	adantr	$⊢ (φ \land M \in ℤ) \to B \subseteq ℤ_{\geq M}$
50		nfv	$⊢ Ⅎ k φ$
51		nfv	$⊢ Ⅎ k m \in B$
52		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in B ⟼ C) (m)$
53	51 52 13	nfif	$⊢ \underline{Ⅎ} k if (m \in B, (k \in B ⟼ C) (m), 0)$
54	10 53	nfeq	$⊢ Ⅎ k (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0)$
55	50 54	nfim	$⊢ Ⅎ k (φ \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0))$
56		eleq1w	$⊢ k = m \to (k \in B \leftrightarrow m \in B)$
57		fveq2	$⊢ k = m \to (k \in B ⟼ C) (k) = (k \in B ⟼ C) (m)$
58	56 57	ifbieq1d	$⊢ k = m \to if (k \in B, (k \in B ⟼ C) (k), 0) = if (m \in B, (k \in B ⟼ C) (m), 0)$
59	16 58	eqeq12d	$⊢ k = m \to ((k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0) \leftrightarrow (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0))$
60	59	imbi2d	$⊢ k = m \to ((φ \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0)) \leftrightarrow (φ \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0)))$
61	25	adantll	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = I (C)$
62	1	adantr	$⊢ (φ \land k \in ℤ_{\geq M}) \to A \subseteq B$
63	62	sselda	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to k \in B$
64		iftrue	$⊢ k \in B \to if (k \in B, (k \in B ⟼ C) (k), 0) = (k \in B ⟼ C) (k)$
65		eqid	$⊢ (k \in B ⟼ C) = (k \in B ⟼ C)$
66	65	fvmpt2i	$⊢ k \in B \to (k \in B ⟼ C) (k) = I (C)$
67	64 66	eqtrd	$⊢ k \in B \to if (k \in B, (k \in B ⟼ C) (k), 0) = I (C)$
68	63 67	syl	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to if (k \in B, (k \in B ⟼ C) (k), 0) = I (C)$
69	61 68	eqtr4d	$⊢ ((φ \land k \in ℤ_{\geq M}) \land k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0)$
70	38	adantll	$⊢ ((φ \land k \in ℤ_{\geq M}) \land \neg k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = 0$
71	67	ad2antrl	$⊢ (φ \land (k \in B \land \neg k \in A)) \to if (k \in B, (k \in B ⟼ C) (k), 0) = I (C)$
72		eldif	$⊢ k \in (B ∖ A) \leftrightarrow (k \in B \land \neg k \in A)$
73	3	fveq2d	$⊢ (φ \land k \in (B ∖ A)) \to I (C) = I (0)$
74		0cn	$⊢ 0 \in ℂ$
75		fvi	$⊢ 0 \in ℂ \to I (0) = 0$
76	74 75	ax-mp	$⊢ I (0) = 0$
77	73 76	eqtrdi	$⊢ (φ \land k \in (B ∖ A)) \to I (C) = 0$
78	72 77	sylan2br	$⊢ (φ \land (k \in B \land \neg k \in A)) \to I (C) = 0$
79	71 78	eqtrd	$⊢ (φ \land (k \in B \land \neg k \in A)) \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0$
80	79	expr	$⊢ (φ \land k \in B) \to (\neg k \in A \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0)$
81		iffalse	$⊢ \neg k \in B \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0$
82	81	adantl	$⊢ (φ \land \neg k \in B) \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0$
83	82	a1d	$⊢ (φ \land \neg k \in B) \to (\neg k \in A \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0)$
84	80 83	pm2.61dan	$⊢ φ \to (\neg k \in A \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0)$
85	84	adantr	$⊢ (φ \land k \in ℤ_{\geq M}) \to (\neg k \in A \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0)$
86	85	imp	$⊢ ((φ \land k \in ℤ_{\geq M}) \land \neg k \in A) \to if (k \in B, (k \in B ⟼ C) (k), 0) = 0$
87	70 86	eqtr4d	$⊢ ((φ \land k \in ℤ_{\geq M}) \land \neg k \in A) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0)$
88	69 87	pm2.61dan	$⊢ (φ \land k \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0)$
89	88	expcom	$⊢ k \in ℤ_{\geq M} \to (φ \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (k) = if (k \in B, (k \in B ⟼ C) (k), 0))$
90	9 55 60 89	vtoclgaf	$⊢ m \in ℤ_{\geq M} \to (φ \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0))$
91	90	impcom	$⊢ (φ \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0)$
92	91	adantlr	$⊢ ((φ \land M \in ℤ) \land m \in ℤ_{\geq M}) \to (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0)) (m) = if (m \in B, (k \in B ⟼ C) (m), 0)$
93	2	ex	$⊢ φ \to (k \in A \to C \in ℂ)$
94	93	adantr	$⊢ (φ \land k \in B) \to (k \in A \to C \in ℂ)$
95	3 74	eqeltrdi	$⊢ (φ \land k \in (B ∖ A)) \to C \in ℂ$
96	72 95	sylan2br	$⊢ (φ \land (k \in B \land \neg k \in A)) \to C \in ℂ$
97	96	expr	$⊢ (φ \land k \in B) \to (\neg k \in A \to C \in ℂ)$
98	94 97	pm2.61d	$⊢ (φ \land k \in B) \to C \in ℂ$
99	98	fmpttd	$⊢ φ \to (k \in B ⟼ C) : B ⟶ ℂ$
100	99	adantr	$⊢ (φ \land M \in ℤ) \to (k \in B ⟼ C) : B ⟶ ℂ$
101	100	ffvelcdmda	$⊢ ((φ \land M \in ℤ) \land m \in B) \to (k \in B ⟼ C) (m) \in ℂ$
102	5 6 49 92 101	zsum	$⊢ (φ \land M \in ℤ) \to \sum_{m \in B} (k \in B ⟼ C) (m) = ⇝ (seq M (+ (k \in ℤ_{\geq M} ⟼ if (k \in A, C, 0))))$
103	48 102	eqtr4d	$⊢ (φ \land M \in ℤ) \to \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{m \in B} (k \in B ⟼ C) (m)$
104		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{k \in A} C$
105		sumfc	$⊢ \sum_{m \in B} (k \in B ⟼ C) (m) = \sum_{k \in B} C$
106	103 104 105	3eqtr3g	$⊢ (φ \land M \in ℤ) \to \sum_{k \in A} C = \sum_{k \in B} C$
107	1	adantr	$⊢ (φ \land \neg M \in ℤ) \to A \subseteq B$
108		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
109	108	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
110	109	eleq2i	$⊢ M \in dom ℤ_{\geq} \leftrightarrow M \in ℤ$
111		ndmfv	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} = \emptyset$
112	110 111	sylnbir	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
113	112	sseq2d	$⊢ \neg M \in ℤ \to (B \subseteq ℤ_{\geq M} \leftrightarrow B \subseteq \emptyset)$
114	4 113	imbitrid	$⊢ \neg M \in ℤ \to (φ \to B \subseteq \emptyset)$
115	114	impcom	$⊢ (φ \land \neg M \in ℤ) \to B \subseteq \emptyset$
116	107 115	sstrd	$⊢ (φ \land \neg M \in ℤ) \to A \subseteq \emptyset$
117		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
118	116 117	syl	$⊢ (φ \land \neg M \in ℤ) \to A = \emptyset$
119		ss0	$⊢ B \subseteq \emptyset \to B = \emptyset$
120	115 119	syl	$⊢ (φ \land \neg M \in ℤ) \to B = \emptyset$
121	118 120	eqtr4d	$⊢ (φ \land \neg M \in ℤ) \to A = B$
122	121	sumeq1d	$⊢ (φ \land \neg M \in ℤ) \to \sum_{k \in A} C = \sum_{k \in B} C$
123	106 122	pm2.61dan	$⊢ φ \to \sum_{k \in A} C = \sum_{k \in B} C$

Metamath Proof Explorer

Theorem sumss

Proof