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 ( 𝜑𝐴𝐵 )
sumss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
sumss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
fsumss.4 ( 𝜑𝐵 ∈ Fin )
Assertion fsumss ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 sumss.1 ( 𝜑𝐴𝐵 )
2 sumss.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 ∈ ℂ )
3 sumss.3 ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
4 fsumss.4 ( 𝜑𝐵 ∈ Fin )
5 1 adantr ( ( 𝜑𝐵 = ∅ ) → 𝐴𝐵 )
6 2 adantlr ( ( ( 𝜑𝐵 = ∅ ) ∧ 𝑘𝐴 ) → 𝐶 ∈ ℂ )
7 3 adantlr ( ( ( 𝜑𝐵 = ∅ ) ∧ 𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 = 0 )
8 simpr ( ( 𝜑𝐵 = ∅ ) → 𝐵 = ∅ )
9 0ss ∅ ⊆ ( ℤ ‘ 0 )
10 8 9 eqsstrdi ( ( 𝜑𝐵 = ∅ ) → 𝐵 ⊆ ( ℤ ‘ 0 ) )
11 5 6 7 10 sumss ( ( 𝜑𝐵 = ∅ ) → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )
12 11 ex ( 𝜑 → ( 𝐵 = ∅ → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 ) )
13 cnvimass ( 𝑓𝐴 ) ⊆ dom 𝑓
14 simprr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 )
15 f1of ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
16 14 15 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
17 13 16 fssdm ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
18 16 ffnd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) )
19 elpreima ( 𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
20 18 19 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
21 16 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
22 21 ex ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
23 22 adantrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
24 20 23 sylbid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) → ( 𝑓𝑛 ) ∈ 𝐵 ) )
25 24 imp ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
26 2 ex ( 𝜑 → ( 𝑘𝐴𝐶 ∈ ℂ ) )
27 26 adantr ( ( 𝜑𝑘𝐵 ) → ( 𝑘𝐴𝐶 ∈ ℂ ) )
28 eldif ( 𝑘 ∈ ( 𝐵𝐴 ) ↔ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) )
29 0cn 0 ∈ ℂ
30 3 29 eqeltrdi ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ ℂ )
31 28 30 sylan2br ( ( 𝜑 ∧ ( 𝑘𝐵 ∧ ¬ 𝑘𝐴 ) ) → 𝐶 ∈ ℂ )
32 31 expr ( ( 𝜑𝑘𝐵 ) → ( ¬ 𝑘𝐴𝐶 ∈ ℂ ) )
33 27 32 pm2.61d ( ( 𝜑𝑘𝐵 ) → 𝐶 ∈ ℂ )
34 33 fmpttd ( 𝜑 → ( 𝑘𝐵𝐶 ) : 𝐵 ⟶ ℂ )
35 34 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑘𝐵𝐶 ) : 𝐵 ⟶ ℂ )
36 35 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐵 ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
37 25 36 syldan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ ℂ )
38 eldifi ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
39 38 21 sylan2 ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑓𝑛 ) ∈ 𝐵 )
40 eldifn ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) → ¬ 𝑛 ∈ ( 𝑓𝐴 ) )
41 40 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ¬ 𝑛 ∈ ( 𝑓𝐴 ) )
42 38 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
43 20 adantr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓𝑛 ) ∈ 𝐴 ) ) )
44 42 43 mpbirand ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑛 ∈ ( 𝑓𝐴 ) ↔ ( 𝑓𝑛 ) ∈ 𝐴 ) )
45 41 44 mtbid ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ¬ ( 𝑓𝑛 ) ∈ 𝐴 )
46 39 45 eldifd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) )
47 difss ( 𝐵𝐴 ) ⊆ 𝐵
48 resmpt ( ( 𝐵𝐴 ) ⊆ 𝐵 → ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) = ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) )
49 47 48 ax-mp ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) = ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 )
50 49 fveq1i ( ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) )
51 fvres ( ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) → ( ( ( 𝑘𝐵𝐶 ) ↾ ( 𝐵𝐴 ) ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
52 50 51 eqtr3id ( ( 𝑓𝑛 ) ∈ ( 𝐵𝐴 ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
53 46 52 syl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
54 c0ex 0 ∈ V
55 54 elsn2 ( 𝐶 ∈ { 0 } ↔ 𝐶 = 0 )
56 3 55 sylibr ( ( 𝜑𝑘 ∈ ( 𝐵𝐴 ) ) → 𝐶 ∈ { 0 } )
57 56 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) : ( 𝐵𝐴 ) ⟶ { 0 } )
58 57 ad2antrr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) : ( 𝐵𝐴 ) ⟶ { 0 } )
59 58 46 ffvelrnd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ { 0 } )
60 elsni ( ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) ∈ { 0 } → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = 0 )
61 59 60 syl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓𝑛 ) ) = 0 )
62 53 61 eqtr3d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( 𝑓𝐴 ) ) ) → ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) = 0 )
63 fzssuz ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ ‘ 1 )
64 63 a1i ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ ‘ 1 ) )
65 17 37 62 64 sumss ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
66 1 ad2antrr ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → 𝐴𝐵 )
67 66 resmptd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) = ( 𝑘𝐴𝐶 ) )
68 67 fveq1d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) )
69 fvres ( 𝑚𝐴 → ( ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
70 69 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( ( 𝑘𝐵𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
71 68 70 eqtr3d ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
72 71 sumeq2dv ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑚𝐴 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
73 fveq2 ( 𝑚 = ( 𝑓𝑛 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
74 fzfid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin )
75 74 16 fisuppfi ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓𝐴 ) ∈ Fin )
76 f1of1 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 )
77 14 76 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 )
78 f1ores ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1𝐵 ∧ ( 𝑓𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) )
79 77 17 78 syl2anc ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) )
80 f1ofo ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵 )
81 14 80 syl ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵 )
82 1 adantr ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → 𝐴𝐵 )
83 foimacnv ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto𝐵𝐴𝐵 ) → ( 𝑓 “ ( 𝑓𝐴 ) ) = 𝐴 )
84 81 82 83 syl2anc ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 “ ( 𝑓𝐴 ) ) = 𝐴 )
85 84 f1oeq3d ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto→ ( 𝑓 “ ( 𝑓𝐴 ) ) ↔ ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto𝐴 ) )
86 79 85 mpbid ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → ( 𝑓 ↾ ( 𝑓𝐴 ) ) : ( 𝑓𝐴 ) –1-1-onto𝐴 )
87 fvres ( 𝑛 ∈ ( 𝑓𝐴 ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) ‘ 𝑛 ) = ( 𝑓𝑛 ) )
88 87 adantl ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 𝑓𝐴 ) ) → ( ( 𝑓 ↾ ( 𝑓𝐴 ) ) ‘ 𝑛 ) = ( 𝑓𝑛 ) )
89 82 sselda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → 𝑚𝐵 )
90 35 ffvelrnda ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐵 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) ∈ ℂ )
91 89 90 syldan ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑚𝐴 ) → ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) ∈ ℂ )
92 73 75 86 88 91 fsumf1o ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = Σ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
93 72 92 eqtrd ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑛 ∈ ( 𝑓𝐴 ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
94 eqidd ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓𝑛 ) = ( 𝑓𝑛 ) )
95 73 74 14 94 90 fsumf1o ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = Σ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘𝐵𝐶 ) ‘ ( 𝑓𝑛 ) ) )
96 65 93 95 3eqtr4d ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) )
97 sumfc Σ 𝑚𝐴 ( ( 𝑘𝐴𝐶 ) ‘ 𝑚 ) = Σ 𝑘𝐴 𝐶
98 sumfc Σ 𝑚𝐵 ( ( 𝑘𝐵𝐶 ) ‘ 𝑚 ) = Σ 𝑘𝐵 𝐶
99 96 97 98 3eqtr3g ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )
100 99 expr ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 ) )
101 100 exlimdv ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 ) )
102 101 expimpd ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 ) )
103 fz1f1o ( 𝐵 ∈ Fin → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) )
104 4 103 syl ( 𝜑 → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto𝐵 ) ) )
105 12 102 104 mpjaod ( 𝜑 → Σ 𝑘𝐴 𝐶 = Σ 𝑘𝐵 𝐶 )