# Metamath Proof Explorer

## Theorem sumss

Description: Change the index set to a subset in an upper integer 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$
sumss.4 ${⊢}{\phi }\to {B}\subseteq {ℤ}_{\ge {M}}$
Assertion sumss ${⊢}{\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 sumss.4 ${⊢}{\phi }\to {B}\subseteq {ℤ}_{\ge {M}}$
5 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
6 simpr ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to {M}\in ℤ$
7 1 4 sstrd ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
8 7 adantr ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to {A}\subseteq {ℤ}_{\ge {M}}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{m}$
10 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)$
11 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{m}\in {A}$
12 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {A}⟼{C}\right)\left({m}\right)$
13 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}0$
14 11 12 13 nfif ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)$
15 10 14 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)$
16 fveq2 ${⊢}{k}={m}\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)$
17 eleq1w ${⊢}{k}={m}\to \left({k}\in {A}↔{m}\in {A}\right)$
18 fveq2 ${⊢}{k}={m}\to \left({k}\in {A}⟼{C}\right)\left({k}\right)=\left({k}\in {A}⟼{C}\right)\left({m}\right)$
19 17 18 ifbieq1d ${⊢}{k}={m}\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)$
20 16 19 eqeq12d ${⊢}{k}={m}\to \left(\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)↔\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)\right)$
21 eqid ${⊢}\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)=\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)$
22 21 fvmpt2i ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=\mathrm{I}\left(if\left({k}\in {A},{C},0\right)\right)$
23 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{C},0\right)={C}$
24 23 fveq2d ${⊢}{k}\in {A}\to \mathrm{I}\left(if\left({k}\in {A},{C},0\right)\right)=\mathrm{I}\left({C}\right)$
25 22 24 sylan9eq ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge {k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=\mathrm{I}\left({C}\right)$
26 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=\left({k}\in {A}⟼{C}\right)\left({k}\right)$
27 eqid ${⊢}\left({k}\in {A}⟼{C}\right)=\left({k}\in {A}⟼{C}\right)$
28 27 fvmpt2i ${⊢}{k}\in {A}\to \left({k}\in {A}⟼{C}\right)\left({k}\right)=\mathrm{I}\left({C}\right)$
29 26 28 eqtrd ${⊢}{k}\in {A}\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=\mathrm{I}\left({C}\right)$
30 29 adantl ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge {k}\in {A}\right)\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=\mathrm{I}\left({C}\right)$
31 25 30 eqtr4d ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge {k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)$
32 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{C},0\right)=0$
33 32 fveq2d ${⊢}¬{k}\in {A}\to \mathrm{I}\left(if\left({k}\in {A},{C},0\right)\right)=\mathrm{I}\left(0\right)$
34 0z ${⊢}0\in ℤ$
35 fvi ${⊢}0\in ℤ\to \mathrm{I}\left(0\right)=0$
36 34 35 ax-mp ${⊢}\mathrm{I}\left(0\right)=0$
37 33 36 syl6eq ${⊢}¬{k}\in {A}\to \mathrm{I}\left(if\left({k}\in {A},{C},0\right)\right)=0$
38 22 37 sylan9eq ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge ¬{k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=0$
39 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=0$
40 39 adantl ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge ¬{k}\in {A}\right)\to if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)=0$
41 38 40 eqtr4d ${⊢}\left({k}\in {ℤ}_{\ge {M}}\wedge ¬{k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)$
42 31 41 pm2.61dan ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {A},\left({k}\in {A}⟼{C}\right)\left({k}\right),0\right)$
43 9 15 20 42 vtoclgaf ${⊢}{m}\in {ℤ}_{\ge {M}}\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)$
44 43 adantl ${⊢}\left(\left({\phi }\wedge {M}\in ℤ\right)\wedge {m}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {A},\left({k}\in {A}⟼{C}\right)\left({m}\right),0\right)$
45 2 fmpttd ${⊢}{\phi }\to \left({k}\in {A}⟼{C}\right):{A}⟶ℂ$
46 45 adantr ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to \left({k}\in {A}⟼{C}\right):{A}⟶ℂ$
47 46 ffvelrnda ${⊢}\left(\left({\phi }\wedge {M}\in ℤ\right)\wedge {m}\in {A}\right)\to \left({k}\in {A}⟼{C}\right)\left({m}\right)\in ℂ$
48 5 6 8 44 47 zsum ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to \sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=⇝\left(seq{M}\left(+,\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\right)\right)$
49 4 adantr ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to {B}\subseteq {ℤ}_{\ge {M}}$
50 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{\phi }$
51 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{m}\in {B}$
52 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {B}⟼{C}\right)\left({m}\right)$
53 51 52 13 nfif ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)$
54 10 53 nfeq ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)$
55 50 54 nfim ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}\left({\phi }\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)\right)$
56 eleq1w ${⊢}{k}={m}\to \left({k}\in {B}↔{m}\in {B}\right)$
57 fveq2 ${⊢}{k}={m}\to \left({k}\in {B}⟼{C}\right)\left({k}\right)=\left({k}\in {B}⟼{C}\right)\left({m}\right)$
58 56 57 ifbieq1d ${⊢}{k}={m}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)$
59 16 58 eqeq12d ${⊢}{k}={m}\to \left(\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)↔\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)\right)$
60 59 imbi2d ${⊢}{k}={m}\to \left(\left({\phi }\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)\right)↔\left({\phi }\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)\right)\right)$
61 25 adantll ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=\mathrm{I}\left({C}\right)$
62 1 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {A}\subseteq {B}$
63 62 sselda ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to {k}\in {B}$
64 iftrue ${⊢}{k}\in {B}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=\left({k}\in {B}⟼{C}\right)\left({k}\right)$
65 eqid ${⊢}\left({k}\in {B}⟼{C}\right)=\left({k}\in {B}⟼{C}\right)$
66 65 fvmpt2i ${⊢}{k}\in {B}\to \left({k}\in {B}⟼{C}\right)\left({k}\right)=\mathrm{I}\left({C}\right)$
67 64 66 eqtrd ${⊢}{k}\in {B}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=\mathrm{I}\left({C}\right)$
68 63 67 syl ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=\mathrm{I}\left({C}\right)$
69 61 68 eqtr4d ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)$
70 38 adantll ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge ¬{k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=0$
71 67 ad2antrl ${⊢}\left({\phi }\wedge \left({k}\in {B}\wedge ¬{k}\in {A}\right)\right)\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=\mathrm{I}\left({C}\right)$
72 eldif ${⊢}{k}\in \left({B}\setminus {A}\right)↔\left({k}\in {B}\wedge ¬{k}\in {A}\right)$
73 3 fveq2d ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to \mathrm{I}\left({C}\right)=\mathrm{I}\left(0\right)$
74 0cn ${⊢}0\in ℂ$
75 fvi ${⊢}0\in ℂ\to \mathrm{I}\left(0\right)=0$
76 74 75 ax-mp ${⊢}\mathrm{I}\left(0\right)=0$
77 73 76 syl6eq ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to \mathrm{I}\left({C}\right)=0$
78 72 77 sylan2br ${⊢}\left({\phi }\wedge \left({k}\in {B}\wedge ¬{k}\in {A}\right)\right)\to \mathrm{I}\left({C}\right)=0$
79 71 78 eqtrd ${⊢}\left({\phi }\wedge \left({k}\in {B}\wedge ¬{k}\in {A}\right)\right)\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0$
80 79 expr ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to \left(¬{k}\in {A}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0\right)$
81 iffalse ${⊢}¬{k}\in {B}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0$
82 81 adantl ${⊢}\left({\phi }\wedge ¬{k}\in {B}\right)\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0$
83 82 a1d ${⊢}\left({\phi }\wedge ¬{k}\in {B}\right)\to \left(¬{k}\in {A}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0\right)$
84 80 83 pm2.61dan ${⊢}{\phi }\to \left(¬{k}\in {A}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0\right)$
85 84 adantr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to \left(¬{k}\in {A}\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0\right)$
86 85 imp ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge ¬{k}\in {A}\right)\to if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)=0$
87 70 86 eqtr4d ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge ¬{k}\in {A}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)$
88 69 87 pm2.61dan ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)$
89 88 expcom ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({\phi }\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({k}\right)=if\left({k}\in {B},\left({k}\in {B}⟼{C}\right)\left({k}\right),0\right)\right)$
90 9 55 60 89 vtoclgaf ${⊢}{m}\in {ℤ}_{\ge {M}}\to \left({\phi }\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)\right)$
91 90 impcom ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)$
92 91 adantlr ${⊢}\left(\left({\phi }\wedge {M}\in ℤ\right)\wedge {m}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\left({m}\right)=if\left({m}\in {B},\left({k}\in {B}⟼{C}\right)\left({m}\right),0\right)$
93 2 ex ${⊢}{\phi }\to \left({k}\in {A}\to {C}\in ℂ\right)$
94 93 adantr ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to \left({k}\in {A}\to {C}\in ℂ\right)$
95 3 74 eqeltrdi ${⊢}\left({\phi }\wedge {k}\in \left({B}\setminus {A}\right)\right)\to {C}\in ℂ$
96 72 95 sylan2br ${⊢}\left({\phi }\wedge \left({k}\in {B}\wedge ¬{k}\in {A}\right)\right)\to {C}\in ℂ$
97 96 expr ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to \left(¬{k}\in {A}\to {C}\in ℂ\right)$
98 94 97 pm2.61d ${⊢}\left({\phi }\wedge {k}\in {B}\right)\to {C}\in ℂ$
99 98 fmpttd ${⊢}{\phi }\to \left({k}\in {B}⟼{C}\right):{B}⟶ℂ$
100 99 adantr ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to \left({k}\in {B}⟼{C}\right):{B}⟶ℂ$
101 100 ffvelrnda ${⊢}\left(\left({\phi }\wedge {M}\in ℤ\right)\wedge {m}\in {B}\right)\to \left({k}\in {B}⟼{C}\right)\left({m}\right)\in ℂ$
102 5 6 49 92 101 zsum ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to \sum _{{m}\in {B}}\left({k}\in {B}⟼{C}\right)\left({m}\right)=⇝\left(seq{M}\left(+,\left({k}\in {ℤ}_{\ge {M}}⟼if\left({k}\in {A},{C},0\right)\right)\right)\right)$
103 48 102 eqtr4d ${⊢}\left({\phi }\wedge {M}\in ℤ\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)$
104 sumfc ${⊢}\sum _{{m}\in {A}}\left({k}\in {A}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {A}}{C}$
105 sumfc ${⊢}\sum _{{m}\in {B}}\left({k}\in {B}⟼{C}\right)\left({m}\right)=\sum _{{k}\in {B}}{C}$
106 103 104 105 3eqtr3g ${⊢}\left({\phi }\wedge {M}\in ℤ\right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$
107 1 adantr ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {A}\subseteq {B}$
108 uzf ${⊢}{ℤ}_{\ge }:ℤ⟶𝒫ℤ$
109 108 fdmi ${⊢}\mathrm{dom}{ℤ}_{\ge }=ℤ$
110 109 eleq2i ${⊢}{M}\in \mathrm{dom}{ℤ}_{\ge }↔{M}\in ℤ$
111 ndmfv ${⊢}¬{M}\in \mathrm{dom}{ℤ}_{\ge }\to {ℤ}_{\ge {M}}=\varnothing$
112 110 111 sylnbir ${⊢}¬{M}\in ℤ\to {ℤ}_{\ge {M}}=\varnothing$
113 112 sseq2d ${⊢}¬{M}\in ℤ\to \left({B}\subseteq {ℤ}_{\ge {M}}↔{B}\subseteq \varnothing \right)$
114 4 113 syl5ib ${⊢}¬{M}\in ℤ\to \left({\phi }\to {B}\subseteq \varnothing \right)$
115 114 impcom ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {B}\subseteq \varnothing$
116 107 115 sstrd ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {A}\subseteq \varnothing$
117 ss0 ${⊢}{A}\subseteq \varnothing \to {A}=\varnothing$
118 116 117 syl ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {A}=\varnothing$
119 ss0 ${⊢}{B}\subseteq \varnothing \to {B}=\varnothing$
120 115 119 syl ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {B}=\varnothing$
121 118 120 eqtr4d ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to {A}={B}$
122 121 sumeq1d ${⊢}\left({\phi }\wedge ¬{M}\in ℤ\right)\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$
123 106 122 pm2.61dan ${⊢}{\phi }\to \sum _{{k}\in {A}}{C}=\sum _{{k}\in {B}}{C}$