| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0cn 11253 | . . . . . . . 8
⊢ 0 ∈
ℂ | 
| 2 |  | fsumrelem.3 | . . . . . . . . 9
⊢ 𝐹:ℂ⟶ℂ | 
| 3 | 2 | ffvelcdmi 7103 | . . . . . . . 8
⊢ (0 ∈
ℂ → (𝐹‘0)
∈ ℂ) | 
| 4 | 1, 3 | ax-mp 5 | . . . . . . 7
⊢ (𝐹‘0) ∈
ℂ | 
| 5 | 4 | addridi 11448 | . . . . . 6
⊢ ((𝐹‘0) + 0) = (𝐹‘0) | 
| 6 |  | fvoveq1 7454 | . . . . . . . . 9
⊢ (𝑥 = 0 → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(0 + 𝑦))) | 
| 7 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑥 = 0 → (𝐹‘𝑥) = (𝐹‘0)) | 
| 8 | 7 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝑥 = 0 → ((𝐹‘𝑥) + (𝐹‘𝑦)) = ((𝐹‘0) + (𝐹‘𝑦))) | 
| 9 | 6, 8 | eqeq12d 2753 | . . . . . . . 8
⊢ (𝑥 = 0 → ((𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦)) ↔ (𝐹‘(0 + 𝑦)) = ((𝐹‘0) + (𝐹‘𝑦)))) | 
| 10 |  | oveq2 7439 | . . . . . . . . . . 11
⊢ (𝑦 = 0 → (0 + 𝑦) = (0 + 0)) | 
| 11 |  | 00id 11436 | . . . . . . . . . . 11
⊢ (0 + 0) =
0 | 
| 12 | 10, 11 | eqtrdi 2793 | . . . . . . . . . 10
⊢ (𝑦 = 0 → (0 + 𝑦) = 0) | 
| 13 | 12 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑦 = 0 → (𝐹‘(0 + 𝑦)) = (𝐹‘0)) | 
| 14 |  | fveq2 6906 | . . . . . . . . . 10
⊢ (𝑦 = 0 → (𝐹‘𝑦) = (𝐹‘0)) | 
| 15 | 14 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑦 = 0 → ((𝐹‘0) + (𝐹‘𝑦)) = ((𝐹‘0) + (𝐹‘0))) | 
| 16 | 13, 15 | eqeq12d 2753 | . . . . . . . 8
⊢ (𝑦 = 0 → ((𝐹‘(0 + 𝑦)) = ((𝐹‘0) + (𝐹‘𝑦)) ↔ (𝐹‘0) = ((𝐹‘0) + (𝐹‘0)))) | 
| 17 |  | fsumrelem.4 | . . . . . . . 8
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 18 | 9, 16, 17 | vtocl2ga 3578 | . . . . . . 7
⊢ ((0
∈ ℂ ∧ 0 ∈ ℂ) → (𝐹‘0) = ((𝐹‘0) + (𝐹‘0))) | 
| 19 | 1, 1, 18 | mp2an 692 | . . . . . 6
⊢ (𝐹‘0) = ((𝐹‘0) + (𝐹‘0)) | 
| 20 | 5, 19 | eqtr2i 2766 | . . . . 5
⊢ ((𝐹‘0) + (𝐹‘0)) = ((𝐹‘0) + 0) | 
| 21 | 4, 4, 1 | addcani 11454 | . . . . 5
⊢ (((𝐹‘0) + (𝐹‘0)) = ((𝐹‘0) + 0) ↔ (𝐹‘0) = 0) | 
| 22 | 20, 21 | mpbi 230 | . . . 4
⊢ (𝐹‘0) = 0 | 
| 23 |  | sumeq1 15725 | . . . . . 6
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) | 
| 24 |  | sum0 15757 | . . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 | 
| 25 | 23, 24 | eqtrdi 2793 | . . . . 5
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = 0) | 
| 26 | 25 | fveq2d 6910 | . . . 4
⊢ (𝐴 = ∅ → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = (𝐹‘0)) | 
| 27 |  | sumeq1 15725 | . . . . 5
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐹‘𝐵) = Σ𝑘 ∈ ∅ (𝐹‘𝐵)) | 
| 28 |  | sum0 15757 | . . . . 5
⊢
Σ𝑘 ∈
∅ (𝐹‘𝐵) = 0 | 
| 29 | 27, 28 | eqtrdi 2793 | . . . 4
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐹‘𝐵) = 0) | 
| 30 | 22, 26, 29 | 3eqtr4a 2803 | . . 3
⊢ (𝐴 = ∅ → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) | 
| 31 | 30 | a1i 11 | . 2
⊢ (𝜑 → (𝐴 = ∅ → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))) | 
| 32 |  | addcl 11237 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 + 𝑦) ∈ ℂ) | 
| 33 | 32 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 + 𝑦) ∈ ℂ) | 
| 34 |  | fsumre.2 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) | 
| 35 | 34 | fmpttd 7135 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) | 
| 37 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) | 
| 38 |  | f1of 6848 | . . . . . . . . . . 11
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) | 
| 40 |  | fco 6760 | . . . . . . . . . 10
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) | 
| 41 | 36, 39, 40 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) | 
| 42 | 41 | ffvelcdmda 7104 | . . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) ∈ ℂ) | 
| 43 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) | 
| 44 |  | nnuz 12921 | . . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) | 
| 45 | 43, 44 | eleqtrdi 2851 | . . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
(ℤ≥‘1)) | 
| 46 | 17 | adantl 481 | . . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) + (𝐹‘𝑦))) | 
| 47 | 39 | ffvelcdmda 7104 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑥) ∈ 𝐴) | 
| 48 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) | 
| 49 |  | eqid 2737 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) | 
| 50 | 49 | fvmpt2 7027 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵) | 
| 51 | 48, 34, 50 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵) | 
| 52 | 51 | fveq2d 6910 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = (𝐹‘𝐵)) | 
| 53 |  | fvex 6919 | . . . . . . . . . . . . . 14
⊢ (𝐹‘𝐵) ∈ V | 
| 54 |  | eqid 2737 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) | 
| 55 | 54 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ V) → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘) = (𝐹‘𝐵)) | 
| 56 | 48, 53, 55 | sylancl 586 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘) = (𝐹‘𝐵)) | 
| 57 | 52, 56 | eqtr4d 2780 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘)) | 
| 58 | 57 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘)) | 
| 59 | 58 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘)) | 
| 60 |  | nfcv 2905 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘𝐹 | 
| 61 |  | nffvmpt1 6917 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥)) | 
| 62 | 60, 61 | nffv 6916 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) | 
| 63 |  | nffvmpt1 6917 | . . . . . . . . . . . 12
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥)) | 
| 64 | 62, 63 | nfeq 2919 | . . . . . . . . . . 11
⊢
Ⅎ𝑘(𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥)) | 
| 65 |  | 2fveq3 6911 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘𝑥) → (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥)))) | 
| 66 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑓‘𝑥) → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥))) | 
| 67 | 65, 66 | eqeq12d 2753 | . . . . . . . . . . 11
⊢ (𝑘 = (𝑓‘𝑥) → ((𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘) ↔ (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥)))) | 
| 68 | 64, 67 | rspc 3610 | . . . . . . . . . 10
⊢ ((𝑓‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘)) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑘) → (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥)))) | 
| 69 | 47, 59, 68 | sylc 65 | . . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥))) | 
| 70 |  | fvco3 7008 | . . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) | 
| 71 | 39, 70 | sylan 580 | . . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) | 
| 72 | 71 | fveq2d 6910 | . . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥)) = (𝐹‘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥)))) | 
| 73 |  | fvco3 7008 | . . . . . . . . . 10
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥))) | 
| 74 | 39, 73 | sylan 580 | . . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∘ 𝑓)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥))) | 
| 75 | 69, 72, 74 | 3eqtr4d 2787 | . . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ (1...(♯‘𝐴))) → (𝐹‘(((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑥)) = (((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∘ 𝑓)‘𝑥)) | 
| 76 | 33, 42, 45, 46, 75 | seqhomo 14090 | . . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝐹‘(seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∘ 𝑓))‘(♯‘𝐴))) | 
| 77 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑥) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑥))) | 
| 78 | 36 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) | 
| 79 | 77, 43, 37, 78, 71 | fsum 15756 | . . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) | 
| 80 | 79 | fveq2d 6910 | . . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝐹‘Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚)) = (𝐹‘(seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴)))) | 
| 81 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑥) → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘(𝑓‘𝑥))) | 
| 82 | 2 | ffvelcdmi 7103 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ ℂ → (𝐹‘𝐵) ∈ ℂ) | 
| 83 | 34, 82 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝐵) ∈ ℂ) | 
| 84 | 83 | fmpttd 7135 | . . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ) | 
| 85 | 84 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)):𝐴⟶ℂ) | 
| 86 | 85 | ffvelcdmda 7104 | . . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑚) ∈ ℂ) | 
| 87 | 81, 43, 37, 86, 74 | fsum 15756 | . . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑚) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵)) ∘ 𝑓))‘(♯‘𝐴))) | 
| 88 | 76, 80, 87 | 3eqtr4d 2787 | . . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝐹‘Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚)) = Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑚)) | 
| 89 |  | sumfc 15745 | . . . . . . 7
⊢
Σ𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵 | 
| 90 | 89 | fveq2i 6909 | . . . . . 6
⊢ (𝐹‘Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚)) = (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) | 
| 91 |  | sumfc 15745 | . . . . . 6
⊢
Σ𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝐵))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵) | 
| 92 | 88, 90, 91 | 3eqtr3g 2800 | . . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) | 
| 93 | 92 | expr 456 | . . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))) | 
| 94 | 93 | exlimdv 1933 | . . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))) | 
| 95 | 94 | expimpd 453 | . 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵))) | 
| 96 |  | fsumre.1 | . . 3
⊢ (𝜑 → 𝐴 ∈ Fin) | 
| 97 |  | fz1f1o 15746 | . . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) | 
| 98 | 96, 97 | syl 17 | . 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) | 
| 99 | 31, 95, 98 | mpjaod 861 | 1
⊢ (𝜑 → (𝐹‘Σ𝑘 ∈ 𝐴 𝐵) = Σ𝑘 ∈ 𝐴 (𝐹‘𝐵)) |