Metamath Proof Explorer

Theorem fsumconst

Description: The sum of constant terms ( k is not free in B ). (Contributed by NM, 24-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion fsumconst ⊢ A ∈ Fin ∧ B ∈ ℂ → ∑ k ∈ A B = A ⁢ B

Proof

Step Hyp Ref Expression
1 mul02 ⊢ B ∈ ℂ → 0 ⋅ B = 0
2 1 adantl ⊢ A ∈ Fin ∧ B ∈ ℂ → 0 ⋅ B = 0
3 2 eqcomd ⊢ A ∈ Fin ∧ B ∈ ℂ → 0 = 0 ⋅ B
4 sumeq1 ⊢ A = ∅ → ∑ k ∈ A B = ∑ k ∈ ∅ B
5 sum0 ⊢ ∑ k ∈ ∅ B = 0
6 4 5 eqtrdi ⊢ A = ∅ → ∑ k ∈ A B = 0
7 fveq2 ⊢ A = ∅ → A = ∅
8 hash0 ⊢ ∅ = 0
9 7 8 eqtrdi ⊢ A = ∅ → A = 0
10 9 oveq1d ⊢ A = ∅ → A ⁢ B = 0 ⋅ B
11 6 10 eqeq12d ⊢ A = ∅ → ∑ k ∈ A B = A ⁢ B ↔ 0 = 0 ⋅ B
12 3 11 syl5ibrcom ⊢ A ∈ Fin ∧ B ∈ ℂ → A = ∅ → ∑ k ∈ A B = A ⁢ B
13 eqidd ⊢ k = f ⁡ n → B = B
14 simprl ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → A ∈ ℕ
15 simprr ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → f : 1 … A ⟶ 1-1 onto A
16 simpllr ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A ∧ k ∈ A → B ∈ ℂ
17 simplr ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → B ∈ ℂ
18 elfznn ⊢ n ∈ 1 … A → n ∈ ℕ
19 fvconst2g ⊢ B ∈ ℂ ∧ n ∈ ℕ → ℕ × B ⁡ n = B
20 17 18 19 syl2an ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A ∧ n ∈ 1 … A → ℕ × B ⁡ n = B
21 13 14 15 16 20 fsum ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → ∑ k ∈ A B = seq 1 + ℕ × B ⁡ A
22 ser1const ⊢ B ∈ ℂ ∧ A ∈ ℕ → seq 1 + ℕ × B ⁡ A = A ⁢ B
23 22 ad2ant2lr ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → seq 1 + ℕ × B ⁡ A = A ⁢ B
24 21 23 eqtrd ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ ∧ f : 1 … A ⟶ 1-1 onto A → ∑ k ∈ A B = A ⁢ B
25 24 expr ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ → f : 1 … A ⟶ 1-1 onto A → ∑ k ∈ A B = A ⁢ B
26 25 exlimdv ⊢ A ∈ Fin ∧ B ∈ ℂ ∧ A ∈ ℕ → ∃ f f : 1 … A ⟶ 1-1 onto A → ∑ k ∈ A B = A ⁢ B
27 26 expimpd ⊢ A ∈ Fin ∧ B ∈ ℂ → A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A → ∑ k ∈ A B = A ⁢ B
28 fz1f1o ⊢ A ∈ Fin → A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A
29 28 adantr ⊢ A ∈ Fin ∧ B ∈ ℂ → A = ∅ ∨ A ∈ ℕ ∧ ∃ f f : 1 … A ⟶ 1-1 onto A
30 12 27 29 mpjaod ⊢ A ∈ Fin ∧ B ∈ ℂ → ∑ k ∈ A B = A ⁢ B