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∈AB=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∈AB=∑k∈∅B
5 sum0 ⊢∑k∈∅B=0
6 4 5 eqtrdi ⊢A=∅→∑k∈AB=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∈AB=A⁢B↔0=0⋅B
12 3 11 syl5ibrcom ⊢A∈Fin∧B∈ℂ→A=∅→∑k∈AB=A⁢B
13 eqidd ⊢k=f⁡n→B=B
14 simprl ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→A∈ℕ
15 simprr ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→f:1…A⟶1-1 ontoA
16 simpllr ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA∧k∈A→B∈ℂ
17 simplr ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→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 ontoA∧n∈1…A→ℕ×B⁡n=B
21 13 14 15 16 20 fsum ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→∑k∈AB=seq1+ℕ×B⁡A
22 ser1const ⊢B∈ℂ∧A∈ℕ→seq1+ℕ×B⁡A=A⁢B
23 22 ad2ant2lr ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→seq1+ℕ×B⁡A=A⁢B
24 21 23 eqtrd ⊢A∈Fin∧B∈ℂ∧A∈ℕ∧f:1…A⟶1-1 ontoA→∑k∈AB=A⁢B
25 24 expr ⊢A∈Fin∧B∈ℂ∧A∈ℕ→f:1…A⟶1-1 ontoA→∑k∈AB=A⁢B
26 25 exlimdv ⊢A∈Fin∧B∈ℂ∧A∈ℕ→∃ff:1…A⟶1-1 ontoA→∑k∈AB=A⁢B
27 26 expimpd ⊢A∈Fin∧B∈ℂ→A∈ℕ∧∃ff:1…A⟶1-1 ontoA→∑k∈AB=A⁢B
28 fz1f1o ⊢A∈Fin→A=∅∨A∈ℕ∧∃ff:1…A⟶1-1 ontoA
29 28 adantr ⊢A∈Fin∧B∈ℂ→A=∅∨A∈ℕ∧∃ff:1…A⟶1-1 ontoA
30 12 27 29 mpjaod ⊢A∈Fin∧B∈ℂ→∑k∈AB=A⁢B