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 ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 mul02 ( 𝐵 ∈ ℂ → ( 0 · 𝐵 ) = 0 )
2 1 adantl ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → ( 0 · 𝐵 ) = 0 )
3 2 eqcomd ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → 0 = ( 0 · 𝐵 ) )
4 sumeq1 ( 𝐴 = ∅ → Σ 𝑘𝐴 𝐵 = Σ 𝑘 ∈ ∅ 𝐵 )
5 sum0 Σ 𝑘 ∈ ∅ 𝐵 = 0
6 4 5 eqtrdi ( 𝐴 = ∅ → Σ 𝑘𝐴 𝐵 = 0 )
7 fveq2 ( 𝐴 = ∅ → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ ∅ ) )
8 hash0 ( ♯ ‘ ∅ ) = 0
9 7 8 eqtrdi ( 𝐴 = ∅ → ( ♯ ‘ 𝐴 ) = 0 )
10 9 oveq1d ( 𝐴 = ∅ → ( ( ♯ ‘ 𝐴 ) · 𝐵 ) = ( 0 · 𝐵 ) )
11 6 10 eqeq12d ( 𝐴 = ∅ → ( Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) ↔ 0 = ( 0 · 𝐵 ) ) )
12 3 11 syl5ibrcom ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → ( 𝐴 = ∅ → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) ) )
13 eqidd ( 𝑘 = ( 𝑓𝑛 ) → 𝐵 = 𝐵 )
14 simprl ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
15 simprr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
16 simpllr ( ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑘𝐴 ) → 𝐵 ∈ ℂ )
17 simplr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → 𝐵 ∈ ℂ )
18 elfznn ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
19 fvconst2g ( ( 𝐵 ∈ ℂ ∧ 𝑛 ∈ ℕ ) → ( ( ℕ × { 𝐵 } ) ‘ 𝑛 ) = 𝐵 )
20 17 18 19 syl2an ( ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ℕ × { 𝐵 } ) ‘ 𝑛 ) = 𝐵 )
21 13 14 15 16 20 fsum ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑘𝐴 𝐵 = ( seq 1 ( + , ( ℕ × { 𝐵 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
22 ser1const ( ( 𝐵 ∈ ℂ ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( seq 1 ( + , ( ℕ × { 𝐵 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) )
23 22 ad2ant2lr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → ( seq 1 ( + , ( ℕ × { 𝐵 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) )
24 21 23 eqtrd ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) )
25 24 expr ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) ) )
26 25 exlimdv ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) ) )
27 26 expimpd ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) ) )
28 fz1f1o ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
29 28 adantr ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
30 12 27 29 mpjaod ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ ℂ ) → Σ 𝑘𝐴 𝐵 = ( ( ♯ ‘ 𝐴 ) · 𝐵 ) )