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 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
sumss.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
sumss.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
sumss.4 ⊢ ( 𝜑 → 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) )
Assertion sumss ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 sumss.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 sumss.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
3 sumss.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
4 sumss.4 ⊢ ( 𝜑 → 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) )
5 eqid ⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
7 1 4 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝐴 ⊆ ( ℤ≥ ‘ 𝑀 ) )
9 nfcv ⊢ Ⅎ 𝑘 𝑚
10 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 )
11 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ 𝐴
12 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 )
13 nfcv ⊢ Ⅎ 𝑘 0
14 11 12 13 nfif ⊢ Ⅎ 𝑘 if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 )
15 10 14 nfeq ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 )
16 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) )
17 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴 ) )
18 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) )
19 17 18 ifbieq1d ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
20 16 19 eqeq12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) ) )
21 eqid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) = ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) )
22 21 fvmpt2i ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) )
23 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 𝐶 )
24 23 fveq2d ⊢ ( 𝑘 ∈ 𝐴 → ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) = ( I ‘ 𝐶 ) )
25 22 24 sylan9eq ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
26 iftrue ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) )
27 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
28 27 fvmpt2i ⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
29 26 28 eqtrd ⊢ ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
30 29 adantl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
31 25 30 eqtr4d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
32 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) = 0 )
33 32 fveq2d ⊢ ( ¬ 𝑘 ∈ 𝐴 → ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) = ( I ‘ 0 ) )
34 0z ⊢ 0 ∈ ℤ
35 fvi ⊢ ( 0 ∈ ℤ → ( I ‘ 0 ) = 0 )
36 34 35 ax-mp ⊢ ( I ‘ 0 ) = 0
37 33 36 eqtrdi ⊢ ( ¬ 𝑘 ∈ 𝐴 → ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) = 0 )
38 22 37 sylan9eq ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = 0 )
39 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
40 39 adantl ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
41 38 40 eqtr4d ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ¬ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
42 31 41 pm2.61dan ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
43 9 15 20 42 vtoclgaf ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐴 , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
45 2 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
47 46 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
48 5 6 8 44 47 zsum ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) )
49 4 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) )
50 nfv ⊢ Ⅎ 𝑘 𝜑
51 nfv ⊢ Ⅎ 𝑘 𝑚 ∈ 𝐵
52 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 )
53 51 52 13 nfif ⊢ Ⅎ 𝑘 if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 )
54 10 53 nfeq ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 )
55 50 54 nfim ⊢ Ⅎ 𝑘 ( 𝜑 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
56 eleq1w ⊢ ( 𝑘 = 𝑚 → ( 𝑘 ∈ 𝐵 ↔ 𝑚 ∈ 𝐵 ) )
57 fveq2 ⊢ ( 𝑘 = 𝑚 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
58 56 57 ifbieq1d ⊢ ( 𝑘 = 𝑚 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
59 16 58 eqeq12d ⊢ ( 𝑘 = 𝑚 → ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) ↔ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) ) )
60 59 imbi2d ⊢ ( 𝑘 = 𝑚 → ( ( 𝜑 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) ) ↔ ( 𝜑 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) ) ) )
61 25 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
62 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ⊆ 𝐵 )
63 62 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐵 )
64 iftrue ⊢ ( 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) )
65 eqid ⊢ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐵 ↦ 𝐶 )
66 65 fvmpt2i ⊢ ( 𝑘 ∈ 𝐵 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) = ( I ‘ 𝐶 ) )
67 64 66 eqtrd ⊢ ( 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
68 63 67 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
69 61 68 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
70 38 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = 0 )
71 67 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) ) → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = ( I ‘ 𝐶 ) )
72 eldif ⊢ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) )
73 3 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( I ‘ 𝐶 ) = ( I ‘ 0 ) )
74 0cn ⊢ 0 ∈ ℂ
75 fvi ⊢ ( 0 ∈ ℂ → ( I ‘ 0 ) = 0 )
76 74 75 ax-mp ⊢ ( I ‘ 0 ) = 0
77 73 76 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( I ‘ 𝐶 ) = 0 )
78 72 77 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) ) → ( I ‘ 𝐶 ) = 0 )
79 71 78 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) ) → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
80 79 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
81 iffalse ⊢ ( ¬ 𝑘 ∈ 𝐵 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
82 81 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐵 ) → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
83 82 a1d ⊢ ( ( 𝜑 ∧ ¬ 𝑘 ∈ 𝐵 ) → ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
84 80 83 pm2.61dan ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 ) )
86 85 imp ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) = 0 )
87 70 86 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ ¬ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
88 69 87 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) )
89 88 expcom ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑘 ) , 0 ) ) )
90 9 55 60 89 vtoclgaf ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝜑 → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) ) )
91 90 impcom ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
92 91 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ‘ 𝑚 ) = if ( 𝑚 ∈ 𝐵 , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) , 0 ) )
93 2 ex ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
95 3 74 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ℂ )
96 72 95 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) ) → 𝐶 ∈ ℂ )
97 96 expr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
98 94 97 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
99 98 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℂ )
100 99 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℂ )
101 100 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) ∧ 𝑚 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
102 5 6 49 92 101 zsum ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = ( ⇝ ‘ seq 𝑀 ( + , ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 0 ) ) ) ) )
103 48 102 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = Σ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
104 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐶
105 sumfc ⊢ Σ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐵 𝐶
106 103 104 105 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )
107 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 ⊆ 𝐵 )
108 uzf ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
109 108 fdmi ⊢ dom ℤ≥ = ℤ
110 109 eleq2i ⊢ ( 𝑀 ∈ dom ℤ≥ ↔ 𝑀 ∈ ℤ )
111 ndmfv ⊢ ( ¬ 𝑀 ∈ dom ℤ≥ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
112 110 111 sylnbir ⊢ ( ¬ 𝑀 ∈ ℤ → ( ℤ≥ ‘ 𝑀 ) = ∅ )
113 112 sseq2d ⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝐵 ⊆ ( ℤ≥ ‘ 𝑀 ) ↔ 𝐵 ⊆ ∅ ) )
114 4 113 syl5ib ⊢ ( ¬ 𝑀 ∈ ℤ → ( 𝜑 → 𝐵 ⊆ ∅ ) )
115 114 impcom ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐵 ⊆ ∅ )
116 107 115 sstrd ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 ⊆ ∅ )
117 ss0 ⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
118 116 117 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 = ∅ )
119 ss0 ⊢ ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
120 115 119 syl ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐵 = ∅ )
121 118 120 eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 = 𝐵 )
122 121 sumeq1d ⊢ ( ( 𝜑 ∧ ¬ 𝑀 ∈ ℤ ) → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )
123 106 122 pm2.61dan ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )