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 ⊢ B ∈ Fin ∧ A ⊆ B → ∑ k ∈ B if k ∈ A 1 0 = A

Proof

Step Hyp Ref Expression
1 ssfi ⊢ B ∈ Fin ∧ A ⊆ B → A ∈ Fin
2 ax-1cn ⊢ 1 ∈ ℂ
3 fsumconst ⊢ A ∈ Fin ∧ 1 ∈ ℂ → ∑ k ∈ A 1 = A ⋅ 1
4 1 2 3 sylancl ⊢ B ∈ Fin ∧ A ⊆ B → ∑ k ∈ A 1 = A ⋅ 1
5 simpr ⊢ B ∈ Fin ∧ A ⊆ B → A ⊆ B
6 2 rgenw ⊢ ∀ k ∈ A 1 ∈ ℂ
7 6 a1i ⊢ B ∈ Fin ∧ A ⊆ B → ∀ k ∈ A 1 ∈ ℂ
8 animorlr ⊢ B ∈ Fin ∧ A ⊆ B → B ⊆ ℤ ≥ C ∨ B ∈ Fin
9 sumss2 ⊢ A ⊆ B ∧ ∀ k ∈ A 1 ∈ ℂ ∧ B ⊆ ℤ ≥ C ∨ B ∈ Fin → ∑ k ∈ A 1 = ∑ k ∈ B if k ∈ A 1 0
10 5 7 8 9 syl21anc ⊢ B ∈ Fin ∧ A ⊆ B → ∑ k ∈ A 1 = ∑ k ∈ B if k ∈ A 1 0
11 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
12 1 11 syl ⊢ B ∈ Fin ∧ A ⊆ B → A ∈ ℕ 0
13 12 nn0cnd ⊢ B ∈ Fin ∧ A ⊆ B → A ∈ ℂ
14 13 mulid1d ⊢ B ∈ Fin ∧ A ⊆ B → A ⋅ 1 = A
15 4 10 14 3eqtr3d ⊢ B ∈ Fin ∧ A ⊆ B → ∑ k ∈ B if k ∈ A 1 0 = A