Metamath Proof Explorer

Theorem fsumadd

Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 22-Apr-2014)

Ref Expression
Hypotheses fsumadd.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumadd.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
fsumadd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
Assertion fsumadd ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fsumadd.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumadd.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 fsumadd.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
4 00id ⊢ ( 0 + 0 ) = 0
5 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
6 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐶 = 0
7 5 6 oveq12i ⊢ ( Σ 𝑘 ∈ ∅ 𝐵 + Σ 𝑘 ∈ ∅ 𝐶 ) = ( 0 + 0 )
8 sum0 ⊢ Σ 𝑘 ∈ ∅ ( 𝐵 + 𝐶 ) = 0
9 4 7 8 3eqtr4ri ⊢ Σ 𝑘 ∈ ∅ ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ ∅ 𝐵 + Σ 𝑘 ∈ ∅ 𝐶 )
10 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = Σ 𝑘 ∈ ∅ ( 𝐵 + 𝐶 ) )
11 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
12 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐶 = Σ 𝑘 ∈ ∅ 𝐶 )
13 11 12 oveq12d ⊢ ( 𝐴 = ∅ → ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) = ( Σ 𝑘 ∈ ∅ 𝐵 + Σ 𝑘 ∈ ∅ 𝐶 ) )
14 9 10 13 3eqtr4a ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) )
15 14 a1i ⊢ ( 𝜑 → ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
17 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
18 16 17 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
19 2 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
20 19 fmpttd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
21 simprr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
22 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
23 21 22 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
24 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
25 20 23 24 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
26 25 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
27 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
28 27 fmpttd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ )
29 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
30 28 23 29 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
31 30 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ∈ ℂ )
32 23 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
33 ovex ⊢ ( 𝐵 + 𝐶 ) ∈ V
34 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) )
35 34 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐵 + 𝐶 ) ∈ V ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( 𝐵 + 𝐶 ) )
36 33 35 mpan2 ⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( 𝐵 + 𝐶 ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( 𝐵 + 𝐶 ) )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
39 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
40 39 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
41 38 2 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
42 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
43 42 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
44 38 3 43 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
45 41 44 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) = ( 𝐵 + 𝐶 ) )
46 37 45 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
47 46 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) )
49 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) )
50 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) )
51 nfcv ⊢ Ⅎ 𝑘 +
52 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) )
53 50 51 52 nfov ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
54 49 53 nfeq ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
55 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
56 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
57 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
58 56 57 oveq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
59 55 58 eqeq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑛 ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) ↔ ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
60 54 59 rspc ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑘 ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) )
61 32 48 60 sylc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
62 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
63 23 62 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
64 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
65 23 64 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
66 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
67 23 66 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
68 65 67 oveq12d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) + ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) + ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ) )
69 61 63 68 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∘ 𝑓 ) ‘ 𝑛 ) = ( ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑛 ) + ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ‘ 𝑛 ) ) )
70 18 26 31 69 seradd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) + ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
71 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
72 19 27 addcld ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
73 72 fmpttd ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) : 𝐴 ⟶ ℂ )
74 73 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑚 ) ∈ ℂ )
75 71 16 21 74 63 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
76 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
77 20 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
78 76 16 21 77 65 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
79 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
80 28 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
81 79 16 21 80 67 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
82 78 81 oveq12d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) + Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) = ( ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) + ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
83 70 75 82 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑚 ) = ( Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) + Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) )
84 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 )
85 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐵
86 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐶
87 85 86 oveq12i ⊢ ( Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) + Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 )
88 83 84 87 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) )
89 88 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) ) )
90 89 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) ) )
91 90 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) ) )
92 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
93 1 92 syl ⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
94 15 91 93 mpjaod ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐵 + 𝐶 ) = ( Σ 𝑘 ∈ 𝐴 𝐵 + Σ 𝑘 ∈ 𝐴 𝐶 ) )