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

Metamath Proof Explorer

Theorem sumhash

Description: The sum of 1 over a set is the size of the set. (Contributed by Mario Carneiro, 8-Mar-2014) (Revised by Mario Carneiro, 20-May-2014)

Ref Expression
Assertion sumhash ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 1 , 0 ) = ( ♯ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ∈ Fin )
2 ax-1cn ⊢ 1 ∈ ℂ
3 fsumconst ⊢ ( ( 𝐴 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ 𝐴 1 = ( ( ♯ ‘ 𝐴 ) · 1 ) )
4 1 2 3 sylancl ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → Σ 𝑘 ∈ 𝐴 1 = ( ( ♯ ‘ 𝐴 ) · 1 ) )
5 simpr ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 ⊆ 𝐵 )
6 2 rgenw ⊢ ∀ 𝑘 ∈ 𝐴 1 ∈ ℂ
7 6 a1i ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ∀ 𝑘 ∈ 𝐴 1 ∈ ℂ )
8 animorlr ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐵 ⊆ ( ℤ≥ ‘ 𝐶 ) ∨ 𝐵 ∈ Fin ) )
9 sumss2 ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ∀ 𝑘 ∈ 𝐴 1 ∈ ℂ ) ∧ ( 𝐵 ⊆ ( ℤ≥ ‘ 𝐶 ) ∨ 𝐵 ∈ Fin ) ) → Σ 𝑘 ∈ 𝐴 1 = Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 1 , 0 ) )
10 5 7 8 9 syl21anc ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → Σ 𝑘 ∈ 𝐴 1 = Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 1 , 0 ) )
11 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
12 1 11 syl ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
13 12 nn0cnd ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ( ♯ ‘ 𝐴 ) ∈ ℂ )
14 13 mulridd ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) · 1 ) = ( ♯ ‘ 𝐴 ) )
15 4 10 14 3eqtr3d ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 1 , 0 ) = ( ♯ ‘ 𝐴 ) )