fsummulc2

Description: A finite sum multiplied by a constant. (Contributed by NM, 12-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		fsummulc2.1	$⊢ φ \to A \in Fin$
2		fsummulc2.2	$⊢ φ \to C \in ℂ$
3		fsummulc2.3	$⊢ (φ \land k \in A) \to B \in ℂ$
4	2	mul01d	$⊢ φ \to C \cdot 0 = 0$
5		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} B = \sum_{k \in \emptyset} B$
6		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
7	5 6	eqtrdi	$⊢ A = \emptyset \to \sum_{k \in A} B = 0$
8	7	oveq2d	$⊢ A = \emptyset \to C \sum_{k \in A} B = C \cdot 0$
9		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} C B = \sum_{k \in \emptyset} C B$
10		sum0	$⊢ \sum_{k \in \emptyset} C B = 0$
11	9 10	eqtrdi	$⊢ A = \emptyset \to \sum_{k \in A} C B = 0$
12	8 11	eqeq12d	$⊢ A = \emptyset \to (C \sum_{k \in A} B = \sum_{k \in A} C B \leftrightarrow C \cdot 0 = 0)$
13	4 12	syl5ibrcom	$⊢ φ \to (A = \emptyset \to C \sum_{k \in A} B = \sum_{k \in A} C B)$
14		addcl	$⊢ (n \in ℂ \land m \in ℂ) \to n + m \in ℂ$
15	14	adantl	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (n \in ℂ \land m \in ℂ)) \to n + m \in ℂ$
16	2	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to C \in ℂ$
17		adddi	$⊢ (C \in ℂ \land n \in ℂ \land m \in ℂ) \to C (n + m) = C n + C m$
18	17	3expb	$⊢ (C \in ℂ \land (n \in ℂ \land m \in ℂ)) \to C (n + m) = C n + C m$
19	16 18	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (n \in ℂ \land m \in ℂ)) \to C (n + m) = C n + C m$
20		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22	20 21	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
23	3	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
24	23	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ B) : A ⟶ ℂ$
25		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
26	25	adantr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
27		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
28	26 27	syl	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f : (1 \dots \|A\|) ⟶ A$
29		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
30	24 28 29	syl2anc	$⊢ ((φ \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) : (1 \dots \|A\|) ⟶ ℂ$
31		simpr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to n \in (1 \dots \|A\|)$
32	30 31	ffvelrnd	$⊢ ((φ \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 ℂ$
33	28 31	ffvelrnd	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to f (n) \in A$
34		simpr	$⊢ (φ \land k \in A) \to k \in A$
35	2	adantr	$⊢ (φ \land k \in A) \to C \in ℂ$
36	35 3	mulcld	$⊢ (φ \land k \in A) \to C B \in ℂ$
37		eqid	$⊢ (k \in A ⟼ C B) = (k \in A ⟼ C B)$
38	37	fvmpt2	$⊢ (k \in A \land C B \in ℂ) \to (k \in A ⟼ C B) (k) = C B$
39	34 36 38	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ C B) (k) = C B$
40		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
41	40	fvmpt2	$⊢ (k \in A \land B \in ℂ) \to (k \in A ⟼ B) (k) = B$
42	34 3 41	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
43	42	oveq2d	$⊢ (φ \land k \in A) \to C (k \in A ⟼ B) (k) = C B$
44	39 43	eqtr4d	$⊢ (φ \land k \in A) \to (k \in A ⟼ C B) (k) = C (k \in A ⟼ B) (k)$
45	44	ralrimiva	$⊢ φ \to \forall k \in A (k \in A ⟼ C B) (k) = C (k \in A ⟼ B) (k)$
46	45	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 ⟼ C B) (k) = C (k \in A ⟼ B) (k)$
47		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ C B) (f (n))$
48		nfcv	$⊢ \underline{Ⅎ} k C$
49		nfcv	$⊢ \underline{Ⅎ} k \times$
50		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (n))$
51	48 49 50	nfov	$⊢ \underline{Ⅎ} k C (k \in A ⟼ B) (f (n))$
52	47 51	nfeq	$⊢ Ⅎ k (k \in A ⟼ C B) (f (n)) = C (k \in A ⟼ B) (f (n))$
53		fveq2	$⊢ k = f (n) \to (k \in A ⟼ C B) (k) = (k \in A ⟼ C B) (f (n))$
54		fveq2	$⊢ k = f (n) \to (k \in A ⟼ B) (k) = (k \in A ⟼ B) (f (n))$
55	54	oveq2d	$⊢ k = f (n) \to C (k \in A ⟼ B) (k) = C (k \in A ⟼ B) (f (n))$
56	53 55	eqeq12d	$⊢ k = f (n) \to ((k \in A ⟼ C B) (k) = C (k \in A ⟼ B) (k) \leftrightarrow (k \in A ⟼ C B) (f (n)) = C (k \in A ⟼ B) (f (n)))$
57	52 56	rspc	$⊢ f (n) \in A \to (\forall k \in A (k \in A ⟼ C B) (k) = C (k \in A ⟼ B) (k) \to (k \in A ⟼ C B) (f (n)) = C (k \in A ⟼ B) (f (n)))$
58	33 46 57	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to (k \in A ⟼ C B) (f (n)) = C (k \in A ⟼ B) (f (n))$
59	27	ad2antll	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
60		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C B) \circ f) (n) = (k \in A ⟼ C B) (f (n))$
61	59 60	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 B) \circ f) (n) = (k \in A ⟼ C B) (f (n))$
62		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))$
63	59 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) \circ f) (n) = (k \in A ⟼ B) (f (n))$
64	63	oveq2d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to C ((k \in A ⟼ B) \circ f) (n) = C (k \in A ⟼ B) (f (n))$
65	58 61 64	3eqtr4d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land n \in (1 \dots \|A\|)) \to ((k \in A ⟼ C B) \circ f) (n) = C ((k \in A ⟼ B) \circ f) (n)$
66	15 19 22 32 65	seqdistr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (+ ((k \in A ⟼ C B) \circ f)) (\|A\|) = C seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
67		fveq2	$⊢ m = f (n) \to (k \in A ⟼ C B) (m) = (k \in A ⟼ C B) (f (n))$
68	36	fmpttd	$⊢ φ \to (k \in A ⟼ C B) : A ⟶ ℂ$
69	68	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ C B) : A ⟶ ℂ$
70	69	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ C B) (m) \in ℂ$
71	67 20 25 70 61	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ C B) (m) = seq 1 (+ ((k \in A ⟼ C B) \circ f)) (\|A\|)$
72		fveq2	$⊢ m = f (n) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (n))$
73	23	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : 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) (m) \in ℂ$
75	72 20 25 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) (m) = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
76	75	oveq2d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to C \sum_{m \in A} (k \in A ⟼ B) (m) = C seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
77	66 71 76	3eqtr4rd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to C \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{m \in A} (k \in A ⟼ C B) (m)$
78		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{k \in A} B$
79	78	oveq2i	$⊢ C \sum_{m \in A} (k \in A ⟼ B) (m) = C \sum_{k \in A} B$
80		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ C B) (m) = \sum_{k \in A} C B$
81	77 79 80	3eqtr3g	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to C \sum_{k \in A} B = \sum_{k \in A} C B$
82	81	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to C \sum_{k \in A} B = \sum_{k \in A} C B)$
83	82	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to C \sum_{k \in A} B = \sum_{k \in A} C B)$
84	83	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to C \sum_{k \in A} B = \sum_{k \in A} C B)$
85		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
86	1 85	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
87	13 84 86	mpjaod	$⊢ φ \to C \sum_{k \in A} B = \sum_{k \in A} C B$

Metamath Proof Explorer

Theorem fsummulc2

Proof