Metamath Proof Explorer

Theorem fsumf1o

Description: Re-index a finite sum using a bijection. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses fsumf1o.1 ⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
fsumf1o.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
fsumf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
fsumf1o.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
fsumf1o.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion fsumf1o ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )

Proof

Step Hyp Ref Expression
1 fsumf1o.1 ⊢ ( 𝑘 = 𝐺 → 𝐵 = 𝐷 )
2 fsumf1o.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
3 fsumf1o.3 ⊢ ( 𝜑 → 𝐹 : 𝐶 –1-1-onto→ 𝐴 )
4 fsumf1o.4 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) = 𝐺 )
5 fsumf1o.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
7 f1oeq2 ⊢ ( 𝐶 = ∅ → ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 ↔ 𝐹 : ∅ –1-1-onto→ 𝐴 ) )
8 3 7 syl5ibcom ⊢ ( 𝜑 → ( 𝐶 = ∅ → 𝐹 : ∅ –1-1-onto→ 𝐴 ) )
9 8 imp ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐹 : ∅ –1-1-onto→ 𝐴 )
10 f1ofo ⊢ ( 𝐹 : ∅ –1-1-onto→ 𝐴 → 𝐹 : ∅ –onto→ 𝐴 )
11 fo00 ⊢ ( 𝐹 : ∅ –onto→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
12 11 simprbi ⊢ ( 𝐹 : ∅ –onto→ 𝐴 → 𝐴 = ∅ )
13 9 10 12 3syl ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐴 = ∅ )
14 13 sumeq1d ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
15 simpr ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → 𝐶 = ∅ )
16 15 sumeq1d ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → Σ 𝑛 ∈ 𝐶 𝐷 = Σ 𝑛 ∈ ∅ 𝐷 )
17 sum0 ⊢ Σ 𝑛 ∈ ∅ 𝐷 = 0
18 16 17 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → Σ 𝑛 ∈ 𝐶 𝐷 = 0 )
19 6 14 18 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝐶 = ∅ ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )
20 19 ex ⊢ ( 𝜑 → ( 𝐶 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 ) )
21 2fveq3 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
22 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( ♯ ‘ 𝐶 ) ∈ ℕ )
23 simprr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 )
24 f1of ⊢ ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 → 𝐹 : 𝐶 ⟶ 𝐴 )
25 3 24 syl ⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐴 )
26 25 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 )
27 5 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
28 27 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
29 26 28 syldan ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ∈ ℂ )
31 f1oco ⊢ ( ( 𝐹 : 𝐶 –1-1-onto→ 𝐴 ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 )
32 3 23 31 syl2an2r ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 )
33 f1of ⊢ ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐴 → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
34 32 33 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 )
35 fvco3 ⊢ ( ( ( 𝐹 ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
36 34 35 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
37 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
38 37 ad2antll ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 )
39 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) ⟶ 𝐶 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) )
40 38 39 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) = ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) )
41 40 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
42 36 41 eqtrd ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐶 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
43 21 22 23 30 42 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → Σ 𝑚 ∈ 𝐶 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
44 25 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐴 )
45 4 44 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → 𝐺 ∈ 𝐴 )
46 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
47 1 46 fvmpti ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
48 45 47 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) = ( I ‘ 𝐷 ) )
49 4 fveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝐺 ) )
50 eqid ⊢ ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) = ( 𝑛 ∈ 𝐶 ↦ 𝐷 )
51 50 fvmpt2i ⊢ ( 𝑛 ∈ 𝐶 → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( I ‘ 𝐷 ) )
53 48 49 52 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) )
55 nffvmpt1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 )
56 55 nfeq1 ⊢ Ⅎ 𝑛 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) )
57 fveq2 ⊢ ( 𝑛 = 𝑚 → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) )
58 2fveq3 ⊢ ( 𝑛 = 𝑚 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
59 57 58 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) ↔ ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
60 56 59 rspc ⊢ ( 𝑚 ∈ 𝐶 → ( ∀ 𝑛 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑛 ) ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) ) )
61 54 60 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐶 ) → ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
63 62 sumeq2dv ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → Σ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = Σ 𝑚 ∈ 𝐶 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝐹 ‘ 𝑚 ) ) )
64 fveq2 ⊢ ( 𝑚 = ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( ( 𝐹 ∘ 𝑓 ) ‘ 𝑛 ) ) )
65 27 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
66 65 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
67 64 22 32 66 36 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ ( 𝐹 ∘ 𝑓 ) ) ) ‘ ( ♯ ‘ 𝐶 ) ) )
68 43 63 67 3eqtr4rd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) )
69 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐵
70 sumfc ⊢ Σ 𝑚 ∈ 𝐶 ( ( 𝑛 ∈ 𝐶 ↦ 𝐷 ) ‘ 𝑚 ) = Σ 𝑛 ∈ 𝐶 𝐷
71 68 69 70 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )
72 71 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 ) )
73 72 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 ) )
74 73 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 ) )
75 fz1f1o ⊢ ( 𝐶 ∈ Fin → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) )
76 2 75 syl ⊢ ( 𝜑 → ( 𝐶 = ∅ ∨ ( ( ♯ ‘ 𝐶 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐶 ) ) –1-1-onto→ 𝐶 ) ) )
77 20 74 76 mpjaod ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑛 ∈ 𝐶 𝐷 )