# Metamath Proof Explorer

## Theorem fsumss

Description: Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses sumss.1 ${⊢}{\phi }\to {A}\subseteq {B}$
sumss.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
sumss.3 ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}=0$
fsumss.4 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
Assertion fsumss ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 sumss.1 ${⊢}{\phi }\to {A}\subseteq {B}$
2 sumss.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {C}\in ℂ$
3 sumss.3 ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}=0$
4 fsumss.4 ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
5 1 adantr ${⊢}\left({\phi }\wedge {B}=\varnothing \right)\to {A}\subseteq {B}$
6 2 adantlr ${⊢}\left(\left({\phi }\wedge {B}=\varnothing \right)\wedge {k}\in {A}\right)\to {C}\in ℂ$
7 3 adantlr ${⊢}\left(\left({\phi }\wedge {B}=\varnothing \right)\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}=0$
8 simpr ${⊢}\left({\phi }\wedge {B}=\varnothing \right)\to {B}=\varnothing$
9 0ss ${⊢}\varnothing \subseteq {ℤ}_{\ge 0}$
10 8 9 eqsstrdi ${⊢}\left({\phi }\wedge {B}=\varnothing \right)\to {B}\subseteq {ℤ}_{\ge 0}$
11 5 6 7 10 sumss ${⊢}\left({\phi }\wedge {B}=\varnothing \right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$
12 11 ex ${⊢}{\phi }\to \left({B}=\varnothing \to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}\right)$
13 cnvimass ${⊢}{{f}}^{-1}\left[{A}\right]\subseteq \mathrm{dom}{f}$
14 simprr ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}$
15 f1of ${⊢}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\to {f}:\left(1\dots \left|{B}\right|\right)⟶{B}$
16 14 15 syl ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}:\left(1\dots \left|{B}\right|\right)⟶{B}$
17 13 16 fssdm ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {{f}}^{-1}\left[{A}\right]\subseteq \left(1\dots \left|{B}\right|\right)$
18 16 ffnd ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}Fn\left(1\dots \left|{B}\right|\right)$
19 elpreima ${⊢}{f}Fn\left(1\dots \left|{B}\right|\right)\to \left({n}\in {{f}}^{-1}\left[{A}\right]↔\left({n}\in \left(1\dots \left|{B}\right|\right)\wedge {f}\left({n}\right)\in {A}\right)\right)$
20 18 19 syl ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({n}\in {{f}}^{-1}\left[{A}\right]↔\left({n}\in \left(1\dots \left|{B}\right|\right)\wedge {f}\left({n}\right)\in {A}\right)\right)$
21 16 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(1\dots \left|{B}\right|\right)\right)\to {f}\left({n}\right)\in {B}$
22 21 ex ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({n}\in \left(1\dots \left|{B}\right|\right)\to {f}\left({n}\right)\in {B}\right)$
23 22 adantrd ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left(\left({n}\in \left(1\dots \left|{B}\right|\right)\wedge {f}\left({n}\right)\in {A}\right)\to {f}\left({n}\right)\in {B}\right)$
24 20 23 sylbid ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({n}\in {{f}}^{-1}\left[{A}\right]\to {f}\left({n}\right)\in {B}\right)$
25 24 imp ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in {{f}}^{-1}\left[{A}\right]\right)\to {f}\left({n}\right)\in {B}$
26 2 ex ${⊢}{\phi }\to \left({k}\in {A}\to {C}\in ℂ\right)$
27 26 adantr ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to \left({k}\in {A}\to {C}\in ℂ\right)$
28 eldif ${⊢}{k}\in \left({B}\setminus {A}\right)↔\left({k}\in {B}\wedge ¬{k}\in {A}\right)$
29 0cn ${⊢}0\in ℂ$
30 3 29 syl6eqel ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}\in ℂ$
31 28 30 sylan2br ${⊢}\left({\phi }\wedge \left({k}\in {B}\wedge ¬{k}\in {A}\right)\right)\to {C}\in ℂ$
32 31 expr ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to \left(¬{k}\in {A}\to {C}\in ℂ\right)$
33 27 32 pm2.61d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {C}\in ℂ$
34 33 fmpttd ${⊢}{\phi }\to \left({k}\in {B}⟼{C}\right):{B}⟶ℂ$
35 34 adantr ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({k}\in {B}⟼{C}\right):{B}⟶ℂ$
36 35 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {f}\left({n}\right)\in {B}\right)\to \left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)\in ℂ$
37 25 36 syldan ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in {{f}}^{-1}\left[{A}\right]\right)\to \left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)\in ℂ$
38 eldifi ${⊢}{n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\to {n}\in \left(1\dots \left|{B}\right|\right)$
39 38 21 sylan2 ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to {f}\left({n}\right)\in {B}$
40 eldifn ${⊢}{n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\to ¬{n}\in {{f}}^{-1}\left[{A}\right]$
41 40 adantl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to ¬{n}\in {{f}}^{-1}\left[{A}\right]$
42 38 adantl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to {n}\in \left(1\dots \left|{B}\right|\right)$
43 20 adantr ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({n}\in {{f}}^{-1}\left[{A}\right]↔\left({n}\in \left(1\dots \left|{B}\right|\right)\wedge {f}\left({n}\right)\in {A}\right)\right)$
44 42 43 mpbirand ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({n}\in {{f}}^{-1}\left[{A}\right]↔{f}\left({n}\right)\in {A}\right)$
45 41 44 mtbid ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to ¬{f}\left({n}\right)\in {A}$
46 39 45 eldifd ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to {f}\left({n}\right)\in \left({B}\setminus {A}\right)$
47 difss ${⊢}{B}\setminus {A}\subseteq {B}$
48 resmpt ${⊢}{B}\setminus {A}\subseteq {B}\to {\left({k}\in {B}⟼{C}\right)↾}_{\left({B}\setminus {A}\right)}=\left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)$
49 47 48 ax-mp ${⊢}{\left({k}\in {B}⟼{C}\right)↾}_{\left({B}\setminus {A}\right)}=\left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)$
50 49 fveq1i ${⊢}\left({\left({k}\in {B}⟼{C}\right)↾}_{\left({B}\setminus {A}\right)}\right)\left({f}\left({n}\right)\right)=\left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)$
51 fvres ${⊢}{f}\left({n}\right)\in \left({B}\setminus {A}\right)\to \left({\left({k}\in {B}⟼{C}\right)↾}_{\left({B}\setminus {A}\right)}\right)\left({f}\left({n}\right)\right)=\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
52 50 51 syl5eqr ${⊢}{f}\left({n}\right)\in \left({B}\setminus {A}\right)\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
53 46 52 syl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)=\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
54 c0ex ${⊢}0\in \mathrm{V}$
55 54 elsn2 ${⊢}{C}\in \left\{0\right\}↔{C}=0$
56 3 55 sylibr ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}\in \left\{0\right\}$
57 56 fmpttd ${⊢}{\phi }\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right):{B}\setminus {A}⟶\left\{0\right\}$
58 57 ad2antrr ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right):{B}\setminus {A}⟶\left\{0\right\}$
59 58 46 ffvelrnd ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)\in \left\{0\right\}$
60 elsni ${⊢}\left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)\in \left\{0\right\}\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)=0$
61 59 60 syl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({k}\in \left({B}\setminus {A}\right)⟼{C}\right)\left({f}\left({n}\right)\right)=0$
62 53 61 eqtr3d ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(\left(1\dots \left|{B}\right|\right)\setminus {{f}}^{-1}\left[{A}\right]\right)\right)\to \left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)=0$
63 fzssuz ${⊢}\left(1\dots \left|{B}\right|\right)\subseteq {ℤ}_{\ge 1}$
64 63 a1i ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left(1\dots \left|{B}\right|\right)\subseteq {ℤ}_{\ge 1}$
65 17 37 62 64 sumss ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{n}\in {{f}}^{-1}\left[{A}\right]}\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)=\sum _{{n}=1}^{\left|{B}\right|}\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
66 1 ad2antrr ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to {A}\subseteq {B}$
67 66 resmptd ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to {\left({k}\in {B}⟼{C}\right)↾}_{{A}}=\left({k}\in {A}⟼{C}\right)$
68 67 fveq1d ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to \left({\left({k}\in {B}⟼{C}\right)↾}_{{A}}\right)\left({m}\right)=\left({k}\in {A}⟼{C}\right)\left({m}\right)$
69 fvres ${⊢}{m}\in {A}\to \left({\left({k}\in {B}⟼{C}\right)↾}_{{A}}\right)\left({m}\right)=\left({k}\in {B}⟼{C}\right)\left({m}\right)$
70 69 adantl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to \left({\left({k}\in {B}⟼{C}\right)↾}_{{A}}\right)\left({m}\right)=\left({k}\in {B}⟼{C}\right)\left({m}\right)$
71 68 70 eqtr3d ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({m}\right)=\left({k}\in {B}⟼{C}\right)\left({m}\right)$
72 71 sumeq2dv ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{m}\in {A}}\left({k}\in {B}⟼{C}\right)\left({m}\right)$
73 fveq2 ${⊢}{m}={f}\left({n}\right)\to \left({k}\in {B}⟼{C}\right)\left({m}\right)=\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
74 fzfid ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left(1\dots \left|{B}\right|\right)\in \mathrm{Fin}$
75 74 16 fisuppfi ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {{f}}^{-1}\left[{A}\right]\in \mathrm{Fin}$
76 f1of1 ${⊢}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\to {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1}{⟶}{B}$
77 14 76 syl ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1}{⟶}{B}$
78 f1ores ${⊢}\left({f}:\left(1\dots \left|{B}\right|\right)\underset{1-1}{⟶}{B}\wedge {{f}}^{-1}\left[{A}\right]\subseteq \left(1\dots \left|{B}\right|\right)\right)\to \left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right):{{f}}^{-1}\left[{A}\right]\underset{1-1 onto}{⟶}{f}\left[{{f}}^{-1}\left[{A}\right]\right]$
79 77 17 78 syl2anc ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right):{{f}}^{-1}\left[{A}\right]\underset{1-1 onto}{⟶}{f}\left[{{f}}^{-1}\left[{A}\right]\right]$
80 f1ofo ${⊢}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\to {f}:\left(1\dots \left|{B}\right|\right)\underset{onto}{⟶}{B}$
81 14 80 syl ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}:\left(1\dots \left|{B}\right|\right)\underset{onto}{⟶}{B}$
82 1 adantr ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {A}\subseteq {B}$
83 foimacnv ${⊢}\left({f}:\left(1\dots \left|{B}\right|\right)\underset{onto}{⟶}{B}\wedge {A}\subseteq {B}\right)\to {f}\left[{{f}}^{-1}\left[{A}\right]\right]={A}$
84 81 82 83 syl2anc ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to {f}\left[{{f}}^{-1}\left[{A}\right]\right]={A}$
85 84 f1oeq3d ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left(\left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right):{{f}}^{-1}\left[{A}\right]\underset{1-1 onto}{⟶}{f}\left[{{f}}^{-1}\left[{A}\right]\right]↔\left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right):{{f}}^{-1}\left[{A}\right]\underset{1-1 onto}{⟶}{A}\right)$
86 79 85 mpbid ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right):{{f}}^{-1}\left[{A}\right]\underset{1-1 onto}{⟶}{A}$
87 fvres ${⊢}{n}\in {{f}}^{-1}\left[{A}\right]\to \left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right)\left({n}\right)={f}\left({n}\right)$
88 87 adantl ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in {{f}}^{-1}\left[{A}\right]\right)\to \left({{f}↾}_{{{f}}^{-1}\left[{A}\right]}\right)\left({n}\right)={f}\left({n}\right)$
89 82 sselda ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to {m}\in {B}$
90 35 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {B}\right)\to \left({k}\in {B}⟼{C}\right)\left({m}\right)\in ℂ$
91 89 90 syldan ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {m}\in {A}\right)\to \left({k}\in {B}⟼{C}\right)\left({m}\right)\in ℂ$
92 73 75 86 88 91 fsumf1o ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {B}⟼{C}\right)\left({m}\right)=\sum _{{n}\in {{f}}^{-1}\left[{A}\right]}\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
93 72 92 eqtrd ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{n}\in {{f}}^{-1}\left[{A}\right]}\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
94 eqidd ${⊢}\left(\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\wedge {n}\in \left(1\dots \left|{B}\right|\right)\right)\to {f}\left({n}\right)={f}\left({n}\right)$
95 73 74 14 94 90 fsumf1o ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{m}\in {B}}\left({k}\in {B}⟼{C}\right)\left({m}\right)=\sum _{{n}=1}^{\left|{B}\right|}\left({k}\in {B}⟼{C}\right)\left({f}\left({n}\right)\right)$
96 65 93 95 3eqtr4d ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{m}\in {B}}\left({k}\in {B}⟼{C}\right)\left({m}\right)$
97 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {A}}{C}$
98 sumfc ${⊢}\sum _{{m}\in {B}}\left({k}\in {B}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {B}}{C}$
99 96 97 98 3eqtr3g ${⊢}\left({\phi }\wedge \left(\left|{B}\right|\in ℕ\wedge {f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$
100 99 expr ${⊢}\left({\phi }\wedge \left|{B}\right|\in ℕ\right)\to \left({f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}\right)$
101 100 exlimdv ${⊢}\left({\phi }\wedge \left|{B}\right|\in ℕ\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}\right)$
102 101 expimpd ${⊢}{\phi }\to \left(\left(\left|{B}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}\right)$
103 fz1f1o ${⊢}{B}\in \mathrm{Fin}\to \left({B}=\varnothing \vee \left(\left|{B}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)$
104 4 103 syl ${⊢}{\phi }\to \left({B}=\varnothing \vee \left(\left|{B}\right|\in ℕ\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}:\left(1\dots \left|{B}\right|\right)\underset{1-1 onto}{⟶}{B}\right)\right)$
105 12 102 104 mpjaod ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$