fsumcl2lem

Description: - Lemma for finite sum closures. (The "-" before "Lemma" forces the math content to be displayed in the Statement List - NM 11-Feb-2008.) (Contributed by Mario Carneiro, 3-Jun-2014)

	Ref	Expression
Hypotheses	fsumcllem.1	$⊢ φ \to S \subseteq ℂ$
	fsumcllem.2	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
	fsumcllem.3	$⊢ φ \to A \in Fin$
	fsumcllem.4	$⊢ (φ \land k \in A) \to B \in S$
	fsumcl2lem.5	$⊢ φ \to A \neq \emptyset$
Assertion	fsumcl2lem	$⊢ φ \to \sum_{k \in A} B \in S$

Proof

Step	Hyp	Ref	Expression
1		fsumcllem.1	$⊢ φ \to S \subseteq ℂ$
2		fsumcllem.2	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
3		fsumcllem.3	$⊢ φ \to A \in Fin$
4		fsumcllem.4	$⊢ (φ \land k \in A) \to B \in S$
5		fsumcl2lem.5	$⊢ φ \to A \neq \emptyset$
6	5	a1d	$⊢ φ \to (\neg \sum_{k \in A} B \in S \to A \neq \emptyset)$
7	6	necon4bd	$⊢ φ \to (A = \emptyset \to \sum_{k \in A} B \in S)$
8		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{k \in A} B$
9		fveq2	$⊢ m = f (x) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (x))$
10		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
11		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
12	1	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to S \subseteq ℂ$
13	4	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ S$
14	13	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ S$
15	14	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in S$
16	12 15	sseldd	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ B) (m) \in ℂ$
17		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
18	11 17	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
19		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) = (k \in A ⟼ B) (f (x))$
20	18 19	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) = (k \in A ⟼ B) (f (x))$
21	9 10 11 16 20	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\|)$
22	8 21	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\|)$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	10 23	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
25		fco	$⊢ ((k \in A ⟼ B) : A ⟶ S \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ S$
26	14 18 25	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ S$
27	26	ffvelcdmda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ B) \circ f) (x) \in S$
28	2	adantlr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (x \in S \land y \in S)) \to x + y \in S$
29	24 27 28	seqcl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|) \in S$
30	22 29	eqeltrd	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{k \in A} B \in S$
31	30	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} B \in S)$
32	31	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} B \in S)$
33	32	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \sum_{k \in A} B \in S)$
34		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
35	3 34	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
36	7 33 35	mpjaod	$⊢ φ \to \sum_{k \in A} B \in S$

Metamath Proof Explorer

Theorem fsumcl2lem

Proof