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	mulid1d	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → ( ( ♯ ‘ 𝐴 ) · 1 ) = ( ♯ ‘ 𝐴 ) )
15	4 10 14	3eqtr3d	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ) → Σ 𝑘 ∈ 𝐵 if ( 𝑘 ∈ 𝐴 , 1 , 0 ) = ( ♯ ‘ 𝐴 ) )