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