fsumrelem

	Ref	Expression
Hypotheses	fsumre.1	$⊢ φ \to A \in Fin$
	fsumre.2	$⊢ (φ \land k \in A) \to B \in ℂ$
	fsumrelem.3	$⊢ F : ℂ ⟶ ℂ$
	fsumrelem.4	$⊢ (x \in ℂ \land y \in ℂ) \to F (x + y) = F (x) + F (y)$
Assertion	fsumrelem	$⊢ φ \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B)$

Proof

Step	Hyp	Ref	Expression
1		fsumre.1	$⊢ φ \to A \in Fin$
2		fsumre.2	$⊢ (φ \land k \in A) \to B \in ℂ$
3		fsumrelem.3	$⊢ F : ℂ ⟶ ℂ$
4		fsumrelem.4	$⊢ (x \in ℂ \land y \in ℂ) \to F (x + y) = F (x) + F (y)$
5		0cn	$⊢ 0 \in ℂ$
6	3	ffvelrni	$⊢ 0 \in ℂ \to F (0) \in ℂ$
7	5 6	ax-mp	$⊢ F (0) \in ℂ$
8	7	addid1i	$⊢ F (0) + 0 = F (0)$
9		fvoveq1	$⊢ x = 0 \to F (x + y) = F (0 + y)$
10		fveq2	$⊢ x = 0 \to F (x) = F (0)$
11	10	oveq1d	$⊢ x = 0 \to F (x) + F (y) = F (0) + F (y)$
12	9 11	eqeq12d	$⊢ x = 0 \to (F (x + y) = F (x) + F (y) \leftrightarrow F (0 + y) = F (0) + F (y))$
13		oveq2	$⊢ y = 0 \to 0 + y = 0 + 0$
14		00id	$⊢ 0 + 0 = 0$
15	13 14	eqtrdi	$⊢ y = 0 \to 0 + y = 0$
16	15	fveq2d	$⊢ y = 0 \to F (0 + y) = F (0)$
17		fveq2	$⊢ y = 0 \to F (y) = F (0)$
18	17	oveq2d	$⊢ y = 0 \to F (0) + F (y) = F (0) + F (0)$
19	16 18	eqeq12d	$⊢ y = 0 \to (F (0 + y) = F (0) + F (y) \leftrightarrow F (0) = F (0) + F (0))$
20	12 19 4	vtocl2ga	$⊢ (0 \in ℂ \land 0 \in ℂ) \to F (0) = F (0) + F (0)$
21	5 5 20	mp2an	$⊢ F (0) = F (0) + F (0)$
22	8 21	eqtr2i	$⊢ F (0) + F (0) = F (0) + 0$
23	7 7 5	addcani	$⊢ F (0) + F (0) = F (0) + 0 \leftrightarrow F (0) = 0$
24	22 23	mpbi	$⊢ F (0) = 0$
25		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} B = \sum_{k \in \emptyset} B$
26		sum0	$⊢ \sum_{k \in \emptyset} B = 0$
27	25 26	eqtrdi	$⊢ A = \emptyset \to \sum_{k \in A} B = 0$
28	27	fveq2d	$⊢ A = \emptyset \to F (\sum_{k \in A} B) = F (0)$
29		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} F (B) = \sum_{k \in \emptyset} F (B)$
30		sum0	$⊢ \sum_{k \in \emptyset} F (B) = 0$
31	29 30	eqtrdi	$⊢ A = \emptyset \to \sum_{k \in A} F (B) = 0$
32	24 28 31	3eqtr4a	$⊢ A = \emptyset \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B)$
33	32	a1i	$⊢ φ \to (A = \emptyset \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B))$
34		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
35	34	adantl	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (x \in ℂ \land y \in ℂ)) \to x + y \in ℂ$
36	2	fmpttd	$⊢ φ \to (k \in A ⟼ B) : A ⟶ ℂ$
37	36	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ B) : A ⟶ ℂ$
38		simprr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
39		f1of	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : (1 \dots \|A\|) ⟶ A$
40	38 39	syl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to f : (1 \dots \|A\|) ⟶ A$
41		fco	$⊢ ((k \in A ⟼ B) : A ⟶ ℂ \land f : (1 \dots \|A\|) ⟶ A) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
42	37 40 41	syl2anc	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to ((k \in A ⟼ B) \circ f) : (1 \dots \|A\|) ⟶ ℂ$
43	42	ffvelrnda	$⊢ ((φ \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 ℂ$
44		simprl	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℕ$
45		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
46	44 45	eleqtrdi	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \|A\| \in ℤ_{\geq 1}$
47	4	adantl	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land (x \in ℂ \land y \in ℂ)) \to F (x + y) = F (x) + F (y)$
48	40	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to f (x) \in A$
49		simpr	$⊢ (φ \land k \in A) \to k \in A$
50		eqid	$⊢ (k \in A ⟼ B) = (k \in A ⟼ B)$
51	50	fvmpt2	$⊢ (k \in A \land B \in ℂ) \to (k \in A ⟼ B) (k) = B$
52	49 2 51	syl2anc	$⊢ (φ \land k \in A) \to (k \in A ⟼ B) (k) = B$
53	52	fveq2d	$⊢ (φ \land k \in A) \to F ((k \in A ⟼ B) (k)) = F (B)$
54		fvex	$⊢ F (B) \in V$
55		eqid	$⊢ (k \in A ⟼ F (B)) = (k \in A ⟼ F (B))$
56	55	fvmpt2	$⊢ (k \in A \land F (B) \in V) \to (k \in A ⟼ F (B)) (k) = F (B)$
57	49 54 56	sylancl	$⊢ (φ \land k \in A) \to (k \in A ⟼ F (B)) (k) = F (B)$
58	53 57	eqtr4d	$⊢ (φ \land k \in A) \to F ((k \in A ⟼ B) (k)) = (k \in A ⟼ F (B)) (k)$
59	58	ralrimiva	$⊢ φ \to \forall k \in A F ((k \in A ⟼ B) (k)) = (k \in A ⟼ F (B)) (k)$
60	59	ad2antrr	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to \forall k \in A F ((k \in A ⟼ B) (k)) = (k \in A ⟼ F (B)) (k)$
61		nfcv	$⊢ \underline{Ⅎ} k F$
62		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ B) (f (x))$
63	61 62	nffv	$⊢ \underline{Ⅎ} k F ((k \in A ⟼ B) (f (x)))$
64		nffvmpt1	$⊢ \underline{Ⅎ} k (k \in A ⟼ F (B)) (f (x))$
65	63 64	nfeq	$⊢ Ⅎ k F ((k \in A ⟼ B) (f (x))) = (k \in A ⟼ F (B)) (f (x))$
66		2fveq3	$⊢ k = f (x) \to F ((k \in A ⟼ B) (k)) = F ((k \in A ⟼ B) (f (x)))$
67		fveq2	$⊢ k = f (x) \to (k \in A ⟼ F (B)) (k) = (k \in A ⟼ F (B)) (f (x))$
68	66 67	eqeq12d	$⊢ k = f (x) \to (F ((k \in A ⟼ B) (k)) = (k \in A ⟼ F (B)) (k) \leftrightarrow F ((k \in A ⟼ B) (f (x))) = (k \in A ⟼ F (B)) (f (x)))$
69	65 68	rspc	$⊢ f (x) \in A \to (\forall k \in A F ((k \in A ⟼ B) (k)) = (k \in A ⟼ F (B)) (k) \to F ((k \in A ⟼ B) (f (x))) = (k \in A ⟼ F (B)) (f (x)))$
70	48 60 69	sylc	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to F ((k \in A ⟼ B) (f (x))) = (k \in A ⟼ F (B)) (f (x))$
71		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))$
72	40 71	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))$
73	72	fveq2d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to F (((k \in A ⟼ B) \circ f) (x)) = F ((k \in A ⟼ B) (f (x)))$
74		fvco3	$⊢ (f : (1 \dots \|A\|) ⟶ A \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ F (B)) \circ f) (x) = (k \in A ⟼ F (B)) (f (x))$
75	40 74	sylan	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to ((k \in A ⟼ F (B)) \circ f) (x) = (k \in A ⟼ F (B)) (f (x))$
76	70 73 75	3eqtr4d	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land x \in (1 \dots \|A\|)) \to F (((k \in A ⟼ B) \circ f) (x)) = ((k \in A ⟼ F (B)) \circ f) (x)$
77	35 43 46 47 76	seqhomo	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to F (seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|)) = seq 1 (+ ((k \in A ⟼ F (B)) \circ f)) (\|A\|)$
78		fveq2	$⊢ m = f (x) \to (k \in A ⟼ B) (m) = (k \in A ⟼ B) (f (x))$
79	37	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 ℂ$
80	78 44 38 79 72	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\|)$
81	80	fveq2d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to F (\sum_{m \in A} (k \in A ⟼ B) (m)) = F (seq 1 (+ ((k \in A ⟼ B) \circ f)) (\|A\|))$
82		fveq2	$⊢ m = f (x) \to (k \in A ⟼ F (B)) (m) = (k \in A ⟼ F (B)) (f (x))$
83	3	ffvelrni	$⊢ B \in ℂ \to F (B) \in ℂ$
84	2 83	syl	$⊢ (φ \land k \in A) \to F (B) \in ℂ$
85	84	fmpttd	$⊢ φ \to (k \in A ⟼ F (B)) : A ⟶ ℂ$
86	85	adantr	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to (k \in A ⟼ F (B)) : A ⟶ ℂ$
87	86	ffvelrnda	$⊢ ((φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \land m \in A) \to (k \in A ⟼ F (B)) (m) \in ℂ$
88	82 44 38 87 75	fsum	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{m \in A} (k \in A ⟼ F (B)) (m) = seq 1 (+ ((k \in A ⟼ F (B)) \circ f)) (\|A\|)$
89	77 81 88	3eqtr4d	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to F (\sum_{m \in A} (k \in A ⟼ B) (m)) = \sum_{m \in A} (k \in A ⟼ F (B)) (m)$
90		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ B) (m) = \sum_{k \in A} B$
91	90	fveq2i	$⊢ F (\sum_{m \in A} (k \in A ⟼ B) (m)) = F (\sum_{k \in A} B)$
92		sumfc	$⊢ \sum_{m \in A} (k \in A ⟼ F (B)) (m) = \sum_{k \in A} F (B)$
93	89 91 92	3eqtr3g	$⊢ (φ \land (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B)$
94	93	expr	$⊢ (φ \land \|A\| \in ℕ) \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B))$
95	94	exlimdv	$⊢ (φ \land \|A\| \in ℕ) \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B))$
96	95	expimpd	$⊢ φ \to ((\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B))$
97		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
98	1 97	syl	$⊢ φ \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
99	33 96 98	mpjaod	$⊢ φ \to F (\sum_{k \in A} B) = \sum_{k \in A} F (B)$

Metamath Proof Explorer

Theorem fsumrelem

Proof