gsumfsum

Description: Relate a group sum on CCfld to a finite sum on the complex numbers. (Contributed by Mario Carneiro, 28-Dec-2014)

	Ref	Expression
Hypotheses	gsumfsum.1	$⊢ φ \to A \in Fin$
	gsumfsum.2	$⊢ (φ \land k \in A) \to B \in ℂ$
Assertion	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		gsumfsum.1	$⊢ φ \to A \in Fin$
2		gsumfsum.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		mpteq1	$⊢ A = \emptyset \to (k \in A ⟼ B) = (k \in \emptyset ⟼ B)$
4		mpt0	$⊢ (k \in \emptyset ⟼ B) = \emptyset$
5	3 4	eqtrdi	$⊢ A = \emptyset \to (k \in A ⟼ B) = \emptyset$
6	5	oveq2d	$⊢ A = \emptyset \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{ℂ_{fld}} \emptyset$
7		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
8	7	gsum0	$⊢ \sum_{ℂ_{fld}} \emptyset = 0$
9		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
10	8 9	eqtr4i	$⊢ \sum_{ℂ_{fld}} \emptyset = \sum_{k \in \emptyset} B$
11	6 10	eqtrdi	$⊢ A = \emptyset \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in \emptyset} B$
12		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} B = \sum_{k \in \emptyset} B$
13	11 12	eqtr4d	$⊢ A = \emptyset \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$
14	13	a1i	$⊢ φ \to (A = \emptyset \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B)$
15		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
16		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
17		eqid	$⊢ Cntz (ℂ_{fld}) = Cntz (ℂ_{fld})$
18		cnring	$⊢ ℂ_{fld} \in Ring$
19		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
20	18 19	mp1i	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ℂ_{fld} \in Mnd$
21	1	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to A \in Fin$
22	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
23	22	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
24		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
25	18 24	mp1i	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ℂ_{fld} \in CMnd$
26	15 17 25 23	cntzcmnf	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ran (k \in A ⟼ B) \subseteq Cntz (ℂ_{fld}) (ran (k \in A ⟼ B))$
27		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
28		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
29		f1of1	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) \underset{1-1}{⟶} A$
30	28 29	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1}{⟶} A$
31		suppssdm	$⊢ (k \in A ⟼ B) supp 0 \subseteq dom (k \in A ⟼ B)$
32	31 23	fssdm	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) supp 0 \subseteq A$
33		f1ofo	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) \underset{onto}{⟶} A$
34		forn	$⊢ f : (1 \dots \|A\|) \underset{onto}{⟶} A \to ran f = A$
35	28 33 34	3syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ran f = A$
36	32 35	sseqtrrd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) supp 0 \subseteq ran f$
37		eqid	$⊢ ((k \in A ⟼ B) \circ f) supp 0 = ((k \in A ⟼ B) \circ f) supp 0$
38	15 7 16 17 20 21 23 26 27 30 36 37	gsumval3	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
39		sumfc	$⊢ \sum_{x \in A} (k \in A ⟼ B) (x) = \sum_{k \in A} B$
40		fveq2	$⊢ x = f (n) \to (k \in A ⟼ B) (x) = (k \in A ⟼ B) (f (n))$
41	23	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in A) \to (k \in A ⟼ B) (x) \in ℂ$
42		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
43	28 42	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
44		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))$
45	43 44	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))$
46	40 27 28 41 45	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{x \in A} (k \in A ⟼ B) (x) = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
47	39 46	eqtr3id	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{k \in A} B = seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)$
48	38 47	eqtr4d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$
49	48	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B)$
50	49	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B)$
51	50	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B)$
52		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
53	1 52	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
54	14 51 53	mpjaod	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} B = \sum_{k \in A} B$

Metamath Proof Explorer

Theorem gsumfsum

Proof