fsumsplit

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

	Ref	Expression
Hypotheses	fsumsplit.1	$⊢ φ \to A \cap B = \emptyset$
	fsumsplit.2	$⊢ φ \to U = A \cup B$
	fsumsplit.3	$⊢ φ \to U \in Fin$
	fsumsplit.4	$⊢ (φ \land k \in U) \to C \in ℂ$
Assertion	fsumsplit	$⊢ φ \to \sum_{k \in U} C = \sum_{k \in A} C + \sum_{k \in B} C$

Proof

Step	Hyp	Ref	Expression
1		fsumsplit.1	$⊢ φ \to A \cap B = \emptyset$
2		fsumsplit.2	$⊢ φ \to U = A \cup B$
3		fsumsplit.3	$⊢ φ \to U \in Fin$
4		fsumsplit.4	$⊢ (φ \land k \in U) \to C \in ℂ$
5		ssun1	$⊢ A \subseteq A \cup B$
6	5 2	sseqtrrid	$⊢ φ \to A \subseteq U$
7	6	sselda	$⊢ (φ \land k \in A) \to k \in U$
8	7 4	syldan	$⊢ (φ \land k \in A) \to C \in ℂ$
9	8	ralrimiva	$⊢ φ \to \forall k \in A C \in ℂ$
10	3	olcd	$⊢ φ \to (U \subseteq ℤ_{\geq 0} \lor U \in Fin)$
11		sumss2	$⊢ ((A \subseteq U \land \forall k \in A C \in ℂ) \land (U \subseteq ℤ_{\geq 0} \lor U \in Fin)) \to \sum_{k \in A} C = \sum_{k \in U} if (k \in A, C, 0)$
12	6 9 10 11	syl21anc	$⊢ φ \to \sum_{k \in A} C = \sum_{k \in U} if (k \in A, C, 0)$
13		ssun2	$⊢ B \subseteq A \cup B$
14	13 2	sseqtrrid	$⊢ φ \to B \subseteq U$
15	14	sselda	$⊢ (φ \land k \in B) \to k \in U$
16	15 4	syldan	$⊢ (φ \land k \in B) \to C \in ℂ$
17	16	ralrimiva	$⊢ φ \to \forall k \in B C \in ℂ$
18		sumss2	$⊢ ((B \subseteq U \land \forall k \in B C \in ℂ) \land (U \subseteq ℤ_{\geq 0} \lor U \in Fin)) \to \sum_{k \in B} C = \sum_{k \in U} if (k \in B, C, 0)$
19	14 17 10 18	syl21anc	$⊢ φ \to \sum_{k \in B} C = \sum_{k \in U} if (k \in B, C, 0)$
20	12 19	oveq12d	$⊢ φ \to \sum_{k \in A} C + \sum_{k \in B} C = \sum_{k \in U} if (k \in A, C, 0) + \sum_{k \in U} if (k \in B, C, 0)$
21		0cn	$⊢ 0 \in ℂ$
22		ifcl	$⊢ (C \in ℂ \land 0 \in ℂ) \to if (k \in A, C, 0) \in ℂ$
23	4 21 22	sylancl	$⊢ (φ \land k \in U) \to if (k \in A, C, 0) \in ℂ$
24		ifcl	$⊢ (C \in ℂ \land 0 \in ℂ) \to if (k \in B, C, 0) \in ℂ$
25	4 21 24	sylancl	$⊢ (φ \land k \in U) \to if (k \in B, C, 0) \in ℂ$
26	3 23 25	fsumadd	$⊢ φ \to \sum_{k \in U} (if (k \in A, C, 0) + if (k \in B, C, 0)) = \sum_{k \in U} if (k \in A, C, 0) + \sum_{k \in U} if (k \in B, C, 0)$
27	2	eleq2d	$⊢ φ \to (k \in U \leftrightarrow k \in (A \cup B))$
28		elun	$⊢ k \in (A \cup B) \leftrightarrow (k \in A \lor k \in B)$
29	27 28	bitrdi	$⊢ φ \to (k \in U \leftrightarrow (k \in A \lor k \in B))$
30	29	biimpa	$⊢ (φ \land k \in U) \to (k \in A \lor k \in B)$
31		iftrue	$⊢ k \in A \to if (k \in A, C, 0) = C$
32	31	adantl	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) = C$
33		noel	$⊢ \neg k \in \emptyset$
34	1	eleq2d	$⊢ φ \to (k \in (A \cap B) \leftrightarrow k \in \emptyset)$
35		elin	$⊢ k \in (A \cap B) \leftrightarrow (k \in A \land k \in B)$
36	34 35	bitr3di	$⊢ φ \to (k \in \emptyset \leftrightarrow (k \in A \land k \in B))$
37	33 36	mtbii	$⊢ φ \to \neg (k \in A \land k \in B)$
38		imnan	$⊢ (k \in A \to \neg k \in B) \leftrightarrow \neg (k \in A \land k \in B)$
39	37 38	sylibr	$⊢ φ \to (k \in A \to \neg k \in B)$
40	39	imp	$⊢ (φ \land k \in A) \to \neg k \in B$
41	40	iffalsed	$⊢ (φ \land k \in A) \to if (k \in B, C, 0) = 0$
42	32 41	oveq12d	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C + 0$
43	8	addid1d	$⊢ (φ \land k \in A) \to C + 0 = C$
44	42 43	eqtrd	$⊢ (φ \land k \in A) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C$
45	39	con2d	$⊢ φ \to (k \in B \to \neg k \in A)$
46	45	imp	$⊢ (φ \land k \in B) \to \neg k \in A$
47	46	iffalsed	$⊢ (φ \land k \in B) \to if (k \in A, C, 0) = 0$
48		iftrue	$⊢ k \in B \to if (k \in B, C, 0) = C$
49	48	adantl	$⊢ (φ \land k \in B) \to if (k \in B, C, 0) = C$
50	47 49	oveq12d	$⊢ (φ \land k \in B) \to if (k \in A, C, 0) + if (k \in B, C, 0) = 0 + C$
51	16	addid2d	$⊢ (φ \land k \in B) \to 0 + C = C$
52	50 51	eqtrd	$⊢ (φ \land k \in B) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C$
53	44 52	jaodan	$⊢ (φ \land (k \in A \lor k \in B)) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C$
54	30 53	syldan	$⊢ (φ \land k \in U) \to if (k \in A, C, 0) + if (k \in B, C, 0) = C$
55	54	sumeq2dv	$⊢ φ \to \sum_{k \in U} (if (k \in A, C, 0) + if (k \in B, C, 0)) = \sum_{k \in U} C$
56	20 26 55	3eqtr2rd	$⊢ φ \to \sum_{k \in U} C = \sum_{k \in A} C + \sum_{k \in B} C$

Metamath Proof Explorer

Theorem fsumsplit

Proof