fsumadd

Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fsumadd.1	$⊢ φ \to A \in Fin$
2		fsumadd.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		fsumadd.3	$⊢ (φ \land k \in A) \to C \in ℂ$
4		00id	$⊢ 0 + 0 = 0$
5		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
6		sum0	$⊢ \sum_{k \in \emptyset} C = 0$
7	5 6	oveq12i	$⊢ \sum_{k \in \emptyset} B + \sum_{k \in \emptyset} C = 0 + 0$
8		sum0	$⊢ \sum_{k \in \emptyset} (B + C) = 0$
9	4 7 8	3eqtr4ri	$⊢ \sum_{k \in \emptyset} (B + C) = \sum_{k \in \emptyset} B + \sum_{k \in \emptyset} C$
10		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} (B + C) = \sum_{k \in \emptyset} (B + C)$
11		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} B = \sum_{k \in \emptyset} B$
12		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} C = \sum_{k \in \emptyset} C$
13	11 12	oveq12d	$⊢ A = \emptyset \to \sum_{k \in A} B + \sum_{k \in A} C = \sum_{k \in \emptyset} B + \sum_{k \in \emptyset} C$
14	9 10 13	3eqtr4a	$⊢ A = \emptyset \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C$
15	14	a1i	$⊢ φ \to (A = \emptyset \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C)$
16		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
17		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
18	16 17	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
19	2	adantlr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to B \in ℂ$
20	19	fmpttd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
21		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
22		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
23	21 22	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
24		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
25	20 23 24	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
26	25	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) \in ℂ$
27	3	adantlr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to C \in ℂ$
28	27	fmpttd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ C) : A ⟶ ℂ$
29		fco	$⊢ ((k \in A ⟼ C) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
30	28 23 29	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ C) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
31	30	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) \in ℂ$
32	23	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f (n) \in A$
33		ovex	$⊢ B + C \in V$
34		eqid	$⊢ (k \in A ⟼ B + C) = (k \in A ⟼ B + C)$
35	34	fvmpt2	$⊢ (k \in A \land B + C \in V) \to (k \in A ⟼ B + C) (k) = B + C$
36	33 35	mpan2	$⊢ k \in A \to (k \in A ⟼ B + C) (k) = B + C$
37	36	adantl	$⊢ (φ \land k \in A) \to (k \in A ⟼ B + C) (k) = B + C$
38		simpr	$⊢ (φ \land k \in A) \to k \in A$
39		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
40	39	fvmpt2	$⊢ (k \in A \land B \in ℂ) \to (k \in A ⟼ B) (k) = B$
41	38 2 40	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
42		eqid	$⊢ (k \in A ⟼ C) = (k \in A ⟼ C)$
43	42	fvmpt2	$⊢ (k \in A \land C \in ℂ) \to (k \in A ⟼ C) (k) = C$
44	38 3 43	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ C) (k) = C$
45	41 44	oveq12d	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k) = B + C$
46	37 45	eqtr4d	$⊢ (φ \land k \in A) \to (k \in A ⟼ B + C) (k) = (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k)$
47	46	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ B + C) (k) = (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k)$
48	47	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to \forall k \in A (k \in A ⟼ B + C) (k) = (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k)$
49		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B + C) (f (n))$
50		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (n))$
51		nfcv	$⊢ \underline{Ⅎ} k +$
52		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C) (f (n))$
53	50 51 52	nfov	$⊢ \underline{Ⅎ} k ((k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n)))$
54	49 53	nfeq	$⊢ Ⅎ k (k \in A ⟼ B + C) (f (n)) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n))$
55		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B + C) (k) = (k \in A ⟼ B + C) (f (n))$
56		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B) (k) = (k \in A ⟼ B) (f (n))$
57		fveq2	$⊢ k = f (n) \to (k \in A ⟼ C) (k) = (k \in A ⟼ C) (f (n))$
58	56 57	oveq12d	$⊢ k = f (n) \to (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n))$
59	55 58	eqeq12d	$⊢ k = f (n) \to ((k \in A ⟼ B + C) (k) = (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k) \leftrightarrow (k \in A ⟼ B + C) (f (n)) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n)))$
60	54 59	rspc	$⊢ f (n) \in A \to (\forall k \in A (k \in A ⟼ B + C) (k) = (k \in A ⟼ B) (k) + (k \in A ⟼ C) (k) \to (k \in A ⟼ B + C) (f (n)) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n)))$
61	32 48 60	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ B + C) (f (n)) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n))$
62		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B + C) \circ f) (n) = (k \in A ⟼ B + C) (f (n))$
63	23 62	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B + C) \circ f) (n) = (k \in A ⟼ B + C) (f (n))$
64		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
65	23 64	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) = (k \in A ⟼ B) (f (n))$
66		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
67	23 66	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ C) (f (n))$
68	65 67	oveq12d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (n) + ((k \in A ⟼ C) \circ f) (n) = (k \in A ⟼ B) (f (n)) + (k \in A ⟼ C) (f (n))$
69	61 63 68	3eqtr4d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ B + C) \circ f) (n) = ((k \in A ⟼ B) \circ f) (n) + ((k \in A ⟼ C) \circ f) (n)$
70	18 26 31 69	seradd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (+ ((k \in A ⟼ B + C) \circ f)) (\|A\|) = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|) + seq 1 (+ ((k \in A ⟼ C) \circ f)) (\|A\|)$
71		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B + C) (m) = (k \in A ⟼ B + C) (f (n))$
72	19 27	addcld	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land k \in A) \to B + C \in ℂ$
73	72	fmpttd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B + C) : A ⟶ ℂ$
74	73	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B + C) (m) \in ℂ$
75	71 16 21 74 63	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ B + C) (m) = seq 1 (+ ((k \in A ⟼ B + C) \circ f)) (\|A\|)$
76		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (n))$
77	20	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
78	76 16 21 77 65	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ B) (m) = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
79		fveq2	$⊢ m = f (n) \to (k \in A ⟼ C) (m) = (k \in A ⟼ C) (f (n))$
80	28	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ C) (m) \in ℂ$
81	79 16 21 80 67	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ C) (m) = seq 1 (+ ((k \in A ⟼ C) \circ f)) (\|A\|)$
82	78 81	oveq12d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ B) (m) + \sum_{m \in A} (k \in A ⟼ C) (m) = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|) + seq 1 (+ ((k \in A ⟼ C) \circ f)) (\|A\|)$
83	70 75 82	3eqtr4d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ B + C) (m) = \sum_{m \in A} (k \in A ⟼ B) (m) + \sum_{m \in A} (k \in A ⟼ C) (m)$
84		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B + C) (m) = \sum_{k \in A} (B + C)$
85		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{k \in A} B$
86		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{k \in A} C$
87	85 86	oveq12i	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) + \sum_{m \in A} (k \in A ⟼ C) (m) = \sum_{k \in A} B + \sum_{k \in A} C$
88	83 84 87	3eqtr3g	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C$
89	88	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C)$
90	89	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C)$
91	90	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C)$
92		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
93	1 92	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
94	15 91 93	mpjaod	$⊢ φ \to \sum_{k \in A} (B + C) = \sum_{k \in A} B + \sum_{k \in A} C$

Metamath Proof Explorer

Theorem fsumadd

Proof