# Metamath Proof Explorer

Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumadd.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fsumadd.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
fsumadd.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
Assertion fsumadd ${⊢}{\phi }\to \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 fsumadd.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fsumadd.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 fsumadd.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
4 00id ${⊢}0+0=0$
5 sum0 ${⊢}\sum _{{k}\in \varnothing }{B}=0$
6 sum0 ${⊢}\sum _{{k}\in \varnothing }{C}=0$
7 5 6 oveq12i ${⊢}\sum _{{k}\in \varnothing }{B}+\sum _{{k}\in \varnothing }{C}=0+0$
8 sum0 ${⊢}\sum _{{k}\in \varnothing }\left({B}+{C}\right)=0$
9 4 7 8 3eqtr4ri ${⊢}\sum _{{k}\in \varnothing }\left({B}+{C}\right)=\sum _{{k}\in \varnothing }{B}+\sum _{{k}\in \varnothing }{C}$
10 sumeq1 ${⊢}{A}=\varnothing \to \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in \varnothing }\left({B}+{C}\right)$
11 sumeq1 ${⊢}{A}=\varnothing \to \sum _{{k}\in {A}}{B}=\sum _{{k}\in \varnothing }{B}$
12 sumeq1 ${⊢}{A}=\varnothing \to \sum _{{k}\in {A}}{C}=\sum _{{k}\in \varnothing }{C}$
13 11 12 oveq12d ${⊢}{A}=\varnothing \to \sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}=\sum _{{k}\in \varnothing }{B}+\sum _{{k}\in \varnothing }{C}$
14 9 10 13 3eqtr4a ${⊢}{A}=\varnothing \to \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}$
15 14 a1i ${⊢}{\phi }\to \left({A}=\varnothing \to \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}\right)$
16 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 ℕ$
17 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
18 16 17 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}$
19 2 adantlr ${⊢}\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 {k}\in {A}\right)\to {B}\in ℂ$
20 19 fmpttd ${⊢}\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}⟶ℂ$
21 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}$
22 f1of ${⊢}{f}:\left(1\dots \left|{A}\right|\right)\underset{1-1 onto}{⟶}{A}\to {f}:\left(1\dots \left|{A}\right|\right)⟶{A}$
23 21 22 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}$
24 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)⟶ℂ$
25 20 23 24 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)⟶ℂ$
26 25 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)\in ℂ$
27 3 adantlr ${⊢}\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 {k}\in {A}\right)\to {C}\in ℂ$
28 27 fmpttd ${⊢}\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}⟼{C}\right):{A}⟶ℂ$
29 fco ${⊢}\left(\left({k}\in {A}⟼{C}\right):{A}⟶ℂ\wedge {f}:\left(1\dots \left|{A}\right|\right)⟶{A}\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
30 28 23 29 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}⟼{C}\right)\circ {f}\right):\left(1\dots \left|{A}\right|\right)⟶ℂ$
31 30 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)\in ℂ$
32 23 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to {f}\left({n}\right)\in {A}$
33 ovex ${⊢}{B}+{C}\in \mathrm{V}$
34 eqid ${⊢}\left({k}\in {A}⟼{B}+{C}\right)=\left({k}\in {A}⟼{B}+{C}\right)$
35 34 fvmpt2 ${⊢}\left({k}\in {A}\wedge {B}+{C}\in \mathrm{V}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)={B}+{C}$
36 33 35 mpan2 ${⊢}{k}\in {A}\to \left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)={B}+{C}$
37 36 adantl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)={B}+{C}$
38 simpr ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {k}\in {A}$
39 eqid ${⊢}\left({k}\in {A}⟼{B}\right)=\left({k}\in {A}⟼{B}\right)$
40 39 fvmpt2 ${⊢}\left({k}\in {A}\wedge {B}\in ℂ\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)={B}$
41 38 2 40 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)={B}$
42 eqid ${⊢}\left({k}\in {A}⟼{C}\right)=\left({k}\in {A}⟼{C}\right)$
43 42 fvmpt2 ${⊢}\left({k}\in {A}\wedge {C}\in ℂ\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
44 38 3 43 syl2anc ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)={C}$
45 41 44 oveq12d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)={B}+{C}$
46 37 45 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)$
47 46 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)$
48 47 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)$
49 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)$
50 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
51 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}+$
52 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
53 50 51 52 nfov ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left(\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)\right)$
54 49 53 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
55 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)$
56 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
57 fveq2 ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{C}\right)\left({k}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
58 56 57 oveq12d ${⊢}{k}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
59 55 58 eqeq12d ${⊢}{k}={f}\left({n}\right)\to \left(\left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)↔\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)\right)$
60 54 59 rspc ${⊢}{f}\left({n}\right)\in {A}\to \left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{B}+{C}\right)\left({k}\right)=\left({k}\in {A}⟼{B}\right)\left({k}\right)+\left({k}\in {A}⟼{C}\right)\left({k}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)\right)$
61 32 48 60 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
62 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}+{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)$
63 23 62 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}+{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)$
64 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
65 23 64 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
66 fvco3 ${⊢}\left({f}:\left(1\dots \left|{A}\right|\right)⟶{A}\wedge {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
67 23 66 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
68 65 67 oveq12d ${⊢}\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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)+\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)+\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
69 61 63 68 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 {n}\in \left(1\dots \left|{A}\right|\right)\right)\to \left(\left({k}\in {A}⟼{B}+{C}\right)\circ {f}\right)\left({n}\right)=\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\left({n}\right)+\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\left({n}\right)$
70 18 26 31 69 seradd ${⊢}\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 seq1\left(+,\left(\left({k}\in {A}⟼{B}+{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)+seq1\left(+,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
71 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}+{C}\right)\left({m}\right)=\left({k}\in {A}⟼{B}+{C}\right)\left({f}\left({n}\right)\right)$
72 19 27 addcld ${⊢}\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 {k}\in {A}\right)\to {B}+{C}\in ℂ$
73 72 fmpttd ${⊢}\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}+{C}\right):{A}⟶ℂ$
74 73 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}+{C}\right)\left({m}\right)\in ℂ$
75 71 16 21 74 63 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}+{C}\right)\left({m}\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}+{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
76 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{B}\right)\left({m}\right)=\left({k}\in {A}⟼{B}\right)\left({f}\left({n}\right)\right)$
77 20 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 ℂ$
78 76 16 21 77 65 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)$
79 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {A}⟼{C}\right)\left({m}\right)=\left({k}\in {A}⟼{C}\right)\left({f}\left({n}\right)\right)$
80 28 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}⟼{C}\right)\left({m}\right)\in ℂ$
81 79 16 21 80 67 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}⟼{C}\right)\left({m}\right)=seq1\left(+,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
82 78 81 oveq12d ${⊢}\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)+\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=seq1\left(+,\left(\left({k}\in {A}⟼{B}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)+seq1\left(+,\left(\left({k}\in {A}⟼{C}\right)\circ {f}\right)\right)\left(\left|{A}\right|\right)$
83 70 75 82 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 \sum _{{m}\in {A}}\left({k}\in {A}⟼{B}+{C}\right)\left({m}\right)=\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)+\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)$
84 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}+{C}\right)\left({m}\right)=\sum _{{k}\in {A}}\left({B}+{C}\right)$
85 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)=\sum _{{k}\in {A}}{B}$
86 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {A}}{C}$
87 85 86 oveq12i ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{B}\right)\left({m}\right)+\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}$
88 83 84 87 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 \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}$
89 88 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 \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}\right)$
90 89 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 \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}\right)$
91 90 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 \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}\right)$
92 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)$
93 1 92 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)$
94 15 91 93 mpjaod ${⊢}{\phi }\to \sum _{{k}\in {A}}\left({B}+{C}\right)=\sum _{{k}\in {A}}{B}+\sum _{{k}\in {A}}{C}$