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 ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ 𝐵 𝐶 )