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 ( 𝜑 → ( 𝐹 ‘ Σ 𝑘𝐴 𝐵 ) = Σ 𝑘𝐴 ( 𝐹𝐵 ) )