sumsplit

Description: Split a sum into two parts. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	sumsplit.1	$⊢ Z = ℤ_{\geq M}$
	sumsplit.2	$⊢ φ \to M \in ℤ$
	sumsplit.3	$⊢ φ \to A \cap B = \emptyset$
	sumsplit.4	$⊢ φ \to A \cup B \subseteq Z$
	sumsplit.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, C, 0)$
	sumsplit.6	$⊢ (φ \land k \in Z) \to G (k) = if (k \in B, C, 0)$
	sumsplit.7	$⊢ (φ \land k \in (A \cup B)) \to C \in ℂ$
	sumsplit.8	$⊢ φ \to seq M (+ F) \in dom ⇝$
	sumsplit.9	$⊢ φ \to seq M (+ G) \in dom ⇝$
Assertion	sumsplit	$⊢ φ \to \sum_{k \in A \cup B} C = \sum_{k \in A} C + \sum_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		sumsplit.1	$⊢ Z = ℤ_{\geq M}$
2		sumsplit.2	$⊢ φ \to M \in ℤ$
3		sumsplit.3	$⊢ φ \to A \cap B = \emptyset$
4		sumsplit.4	$⊢ φ \to A \cup B \subseteq Z$
5		sumsplit.5	$⊢ (φ \land k \in Z) \to F (k) = if (k \in A, C, 0)$
6		sumsplit.6	$⊢ (φ \land k \in Z) \to G (k) = if (k \in B, C, 0)$
7		sumsplit.7	$⊢ (φ \land k \in (A \cup B)) \to C \in ℂ$
8		sumsplit.8	$⊢ φ \to seq M (+ F) \in dom ⇝$
9		sumsplit.9	$⊢ φ \to seq M (+ G) \in dom ⇝$
10	7	ralrimiva	$⊢ φ \to \forall k \in (A \cup B) C \in ℂ$
11	1	eqimssi	$⊢ Z \subseteq ℤ_{\geq M}$
12	11	a1i	$⊢ φ \to Z \subseteq ℤ_{\geq M}$
13	12	orcd	$⊢ φ \to (Z \subseteq ℤ_{\geq M} \lor Z \in Fin)$
14		sumss2	$⊢ ((A \cup B \subseteq Z \land \forall k \in (A \cup B) C \in ℂ) \land (Z \subseteq ℤ_{\geq M} \lor Z \in Fin)) \to \sum_{k \in A \cup B} C = \sum_{k \in Z} if (k \in (A \cup B), C, 0)$
15	4 10 13 14	syl21anc	$⊢ φ \to \sum_{k \in A \cup B} C = \sum_{k \in Z} if (k \in (A \cup B), C, 0)$
16		iftrue	$⊢ k \in A \to if (k \in A, C, 0) = C$
17	16	adantl	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) = C$
18		elun1	$⊢ k \in A \to k \in (A \cup B)$
19	18 7	sylan2	$⊢ (φ \land k \in A) \to C \in ℂ$
20	17 19	eqeltrd	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) \in ℂ$
21		iffalse	$⊢ \neg k \in A \to if (k \in A, C, 0) = 0$
22		0cn	$⊢ 0 \in ℂ$
23	21 22	eqeltrdi	$⊢ \neg k \in A \to if (k \in A, C, 0) \in ℂ$
24	23	adantl	$⊢ (φ \land \neg k \in A) \to if (k \in A, C, 0) \in ℂ$
25	20 24	pm2.61dan	$⊢ φ \to if (k \in A, C, 0) \in ℂ$
26	25	adantr	$⊢ (φ \land k \in Z) \to if (k \in A, C, 0) \in ℂ$
27		iftrue	$⊢ k \in B \to if (k \in B, C, 0) = C$
28	27	adantl	$⊢ (φ \land k \in B) \to if (k \in B, C, 0) = C$
29		elun2	$⊢ k \in B \to k \in (A \cup B)$
30	29 7	sylan2	$⊢ (φ \land k \in B) \to C \in ℂ$
31	28 30	eqeltrd	$⊢ (φ \land k \in B) \to if (k \in B, C, 0) \in ℂ$
32		iffalse	$⊢ \neg k \in B \to if (k \in B, C, 0) = 0$
33	32 22	eqeltrdi	$⊢ \neg k \in B \to if (k \in B, C, 0) \in ℂ$
34	33	adantl	$⊢ (φ \land \neg k \in B) \to if (k \in B, C, 0) \in ℂ$
35	31 34	pm2.61dan	$⊢ φ \to if (k \in B, C, 0) \in ℂ$
36	35	adantr	$⊢ (φ \land k \in Z) \to if (k \in B, C, 0) \in ℂ$
37	1 2 5 26 6 36 8 9	isumadd	$⊢ φ \to \sum_{k \in Z} (if (k \in A, C, 0) + if (k \in B, C, 0)) = \sum_{k \in Z} if (k \in A, C, 0) + \sum_{k \in Z} if (k \in B, C, 0)$
38	19	addridd	$⊢ (φ \land k \in A) \to C + 0 = C$
39		noel	$⊢ \neg k \in \emptyset$
40	3	eleq2d	$⊢ φ \to (k \in (A \cap B) \leftrightarrow k \in \emptyset)$
41		elin	$⊢ k \in (A \cap B) \leftrightarrow (k \in A \land k \in B)$
42	40 41	bitr3di	$⊢ φ \to (k \in \emptyset \leftrightarrow (k \in A \land k \in B))$
43	39 42	mtbii	$⊢ φ \to \neg (k \in A \land k \in B)$
44		imnan	$⊢ (k \in A \to \neg k \in B) \leftrightarrow \neg (k \in A \land k \in B)$
45	43 44	sylibr	$⊢ φ \to (k \in A \to \neg k \in B)$
46	45	imp	$⊢ (φ \land k \in A) \to \neg k \in B$
47	46 32	syl	$⊢ (φ \land k \in A) \to if (k \in B, C, 0) = 0$
48	17 47	oveq12d	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C + 0$
49		iftrue	$⊢ k \in (A \cup B) \to if (k \in (A \cup B), C, 0) = C$
50	18 49	syl	$⊢ k \in A \to if (k \in (A \cup B), C, 0) = C$
51	50	adantl	$⊢ (φ \land k \in A) \to if (k \in (A \cup B), C, 0) = C$
52	38 48 51	3eqtr4rd	$⊢ (φ \land k \in A) \to if (k \in (A \cup B), C, 0) = if (k \in A, C, 0) + if (k \in B, C, 0)$
53	35	addlidd	$⊢ φ \to 0 + if (k \in B, C, 0) = if (k \in B, C, 0)$
54	53	adantr	$⊢ (φ \land \neg k \in A) \to 0 + if (k \in B, C, 0) = if (k \in B, C, 0)$
55	21	adantl	$⊢ (φ \land \neg k \in A) \to if (k \in A, C, 0) = 0$
56	55	oveq1d	$⊢ (φ \land \neg k \in A) \to if (k \in A, C, 0) + if (k \in B, C, 0) = 0 + if (k \in B, C, 0)$
57		elun	$⊢ k \in (A \cup B) \leftrightarrow (k \in A \lor k \in B)$
58		biorf	$⊢ \neg k \in A \to (k \in B \leftrightarrow (k \in A \lor k \in B))$
59	57 58	bitr4id	$⊢ \neg k \in A \to (k \in (A \cup B) \leftrightarrow k \in B)$
60	59	adantl	$⊢ (φ \land \neg k \in A) \to (k \in (A \cup B) \leftrightarrow k \in B)$
61	60	ifbid	$⊢ (φ \land \neg k \in A) \to if (k \in (A \cup B), C, 0) = if (k \in B, C, 0)$
62	54 56 61	3eqtr4rd	$⊢ (φ \land \neg k \in A) \to if (k \in (A \cup B), C, 0) = if (k \in A, C, 0) + if (k \in B, C, 0)$
63	52 62	pm2.61dan	$⊢ φ \to if (k \in (A \cup B), C, 0) = if (k \in A, C, 0) + if (k \in B, C, 0)$
64	63	sumeq2sdv	$⊢ φ \to \sum_{k \in Z} if (k \in (A \cup B), C, 0) = \sum_{k \in Z} (if (k \in A, C, 0) + if (k \in B, C, 0))$
65	4	unssad	$⊢ φ \to A \subseteq Z$
66	19	ralrimiva	$⊢ φ \to \forall k \in A C \in ℂ$
67		sumss2	$⊢ ((A \subseteq Z \land \forall k \in A C \in ℂ) \land (Z \subseteq ℤ_{\geq M} \lor Z \in Fin)) \to \sum_{k \in A} C = \sum_{k \in Z} if (k \in A, C, 0)$
68	65 66 13 67	syl21anc	$⊢ φ \to \sum_{k \in A} C = \sum_{k \in Z} if (k \in A, C, 0)$
69	4	unssbd	$⊢ φ \to B \subseteq Z$
70	30	ralrimiva	$⊢ φ \to \forall k \in B C \in ℂ$
71		sumss2	$⊢ ((B \subseteq Z \land \forall k \in B C \in ℂ) \land (Z \subseteq ℤ_{\geq M} \lor Z \in Fin)) \to \sum_{k \in B} C = \sum_{k \in Z} if (k \in B, C, 0)$
72	69 70 13 71	syl21anc	$⊢ φ \to \sum_{k \in B} C = \sum_{k \in Z} if (k \in B, C, 0)$
73	68 72	oveq12d	$⊢ φ \to \sum_{k \in A} C + \sum_{k \in B} C = \sum_{k \in Z} if (k \in A, C, 0) + \sum_{k \in Z} if (k \in B, C, 0)$
74	37 64 73	3eqtr4rd	$⊢ φ \to \sum_{k \in A} C + \sum_{k \in B} C = \sum_{k \in Z} if (k \in (A \cup B), C, 0)$
75	15 74	eqtr4d	$⊢ φ \to \sum_{k \in A \cup B} C = \sum_{k \in A} C + \sum_{k \in B} C$

Metamath Proof Explorer

Theorem sumsplit

Proof