# Metamath Proof Explorer

## Theorem fsumrelem

Description: Lemma for fsumre , fsumim , and fsumcj . (Contributed by Mario Carneiro, 25-Jul-2014) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses fsumre.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumre.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fsumrelem.3 ${⊢}{F}:ℂ⟶ℂ$
fsumrelem.4 ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\right)\to {F}\left({x}+{y}\right)={F}\left({x}\right)+{F}\left({y}\right)$
Assertion fsumrelem ${⊢}{\phi }\to {F}\left(\sum _{{k}\in {A}}{B}\right)=\sum _{{k}\in {A}}{F}\left({B}\right)$

### Proof

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