Metamath Proof Explorer

Theorem fsumrelem

Description: Lemma for fsumre , fsumim , and fsumcj . (Contributed by Mario Carneiro, 25-Jul-2014) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypotheses fsumre.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumre.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
fsumrelem.3 ⊢ 𝐹 : ℂ ⟶ ℂ
fsumrelem.4 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
Assertion fsumrelem ( 𝜑 → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fsumre.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumre.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3 fsumrelem.3 ⊢ 𝐹 : ℂ ⟶ ℂ
4 fsumrelem.4 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
5 0cn ⊢ 0 ∈ ℂ
6 3 ffvelrni ⊢ ( 0 ∈ ℂ → ( 𝐹 ‘ 0 ) ∈ ℂ )
7 5 6 ax-mp ⊢ ( 𝐹 ‘ 0 ) ∈ ℂ
8 7 addid1i ⊢ ( ( 𝐹 ‘ 0 ) + 0 ) = ( 𝐹 ‘ 0 )
9 fvoveq1 ⊢ ( 𝑥 = 0 → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 0 + 𝑦 ) ) )
10 fveq2 ⊢ ( 𝑥 = 0 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 0 ) )
11 10 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) )
12 9 11 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 0 + 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) ) )
13 oveq2 ⊢ ( 𝑦 = 0 → ( 0 + 𝑦 ) = ( 0 + 0 ) )
14 00id ⊢ ( 0 + 0 ) = 0
15 13 14 eqtrdi ⊢ ( 𝑦 = 0 → ( 0 + 𝑦 ) = 0 )
16 15 fveq2d ⊢ ( 𝑦 = 0 → ( 𝐹 ‘ ( 0 + 𝑦 ) ) = ( 𝐹 ‘ 0 ) )
17 fveq2 ⊢ ( 𝑦 = 0 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 0 ) )
18 17 oveq2d ⊢ ( 𝑦 = 0 → ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑦 = 0 → ( ( 𝐹 ‘ ( 0 + 𝑦 ) ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ 0 ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) ) ) )
20 12 19 4 vtocl2ga ⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) ) )
21 5 5 20 mp2an ⊢ ( 𝐹 ‘ 0 ) = ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) )
22 8 21 eqtr2i ⊢ ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) ) = ( ( 𝐹 ‘ 0 ) + 0 )
23 7 7 5 addcani ⊢ ( ( ( 𝐹 ‘ 0 ) + ( 𝐹 ‘ 0 ) ) = ( ( 𝐹 ‘ 0 ) + 0 ) ↔ ( 𝐹 ‘ 0 ) = 0 )
24 22 23 mpbi ⊢ ( 𝐹 ‘ 0 ) = 0
25 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
26 sum0 ⊢ Σ 𝑘 ∈ ∅ 𝐵 = 0
27 25 26 eqtrdi ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 𝐵 = 0 )
28 27 fveq2d ⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = ( 𝐹 ‘ 0 ) )
29 sumeq1 ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) = Σ 𝑘 ∈ ∅ ( 𝐹 ‘ 𝐵 ) )
30 sum0 ⊢ Σ 𝑘 ∈ ∅ ( 𝐹 ‘ 𝐵 ) = 0
31 29 30 eqtrdi ⊢ ( 𝐴 = ∅ → Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) = 0 )
32 24 28 31 3eqtr4a ⊢ ( 𝐴 = ∅ → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) )
33 32 a1i ⊢ ( 𝜑 → ( 𝐴 = ∅ → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) ) )
34 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
36 2 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
37 36 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
38 simprr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
39 f1of ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
40 38 39 syl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
41 fco ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
42 37 40 41 syl2anc ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ ℂ )
43 42 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) ∈ ℂ )
44 simprl ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
45 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
46 44 45 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
47 4 adantl ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
48 40 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 )
49 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
50 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
51 50 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
52 49 2 51 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) = 𝐵 )
53 52 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ 𝐵 ) )
54 fvex ⊢ ( 𝐹 ‘ 𝐵 ) ∈ V
55 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) )
56 55 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝐵 ) ∈ V ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝐵 ) )
57 49 54 56 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝐵 ) )
58 53 57 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) )
59 58 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) )
61 nfcv ⊢ Ⅎ 𝑘 𝐹
62 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) )
63 61 62 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
64 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) )
65 63 64 nfeq ⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) )
66 2fveq3 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
67 fveq2 ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
68 66 67 eqeq12d ⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
69 65 68 rspc ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑘 ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑘 ) → ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
70 48 60 69 sylc ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
71 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
72 40 71 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
73 72 fveq2d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
74 fvco3 ⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
75 40 74 sylan ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑥 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
76 70 73 75 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑥 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( 𝐹 ‘ ( ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ‘ 𝑥 ) ) = ( ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∘ 𝑓 ) ‘ 𝑥 ) )
77 35 43 46 47 76 seqhomo ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐹 ‘ ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
78 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
79 37 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ∈ ℂ )
80 78 44 38 79 72 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
81 80 fveq2d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐹 ‘ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐹 ‘ ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) ) )
82 fveq2 ⊢ ( 𝑚 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ ( 𝑓 ‘ 𝑥 ) ) )
83 3 ffvelrni ⊢ ( 𝐵 ∈ ℂ → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
84 2 83 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ∈ ℂ )
85 84 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
86 85 adantr ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
87 86 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑚 ) ∈ ℂ )
88 82 44 38 87 75 fsum ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( + , ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
89 77 81 88 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐹 ‘ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑚 ) )
90 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 𝐵
91 90 fveq2i ⊢ ( 𝐹 ‘ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑚 ) ) = ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 )
92 sumfc ⊢ Σ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) ‘ 𝑚 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 )
93 89 91 92 3eqtr3g ⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) )
94 93 expr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) ) )
95 94 exlimdv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) ) )
96 95 expimpd ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) ) )
97 fz1f1o ⊢ ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
98 1 97 syl ⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 ) ) )
99 33 96 98 mpjaod ⊢ ( 𝜑 → ( 𝐹 ‘ Σ 𝑘 ∈ 𝐴 𝐵 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝐵 ) )