This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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