Metamath Proof Explorer

Theorem indsumhash

Description: The finite sum of the indicator function is the number of elements of the corresponding subset. (Contributed by AV, 10-Apr-2026)

Ref Expression
Hypothesis indsumhash.f ⊢ 1 ˙ = 𝟙 O ⁡ A
Assertion indsumhash ⊢ O ∈ Fin ∧ A ⊆ O → ∑ k ∈ O 1 ˙ ⁡ k = A

Proof

Step Hyp Ref Expression
1 indsumhash.f ⊢ 1 ˙ = 𝟙 O ⁡ A
2 1 fveq1i ⊢ 1 ˙ ⁡ k = 𝟙 O ⁡ A ⁡ k
3 fvindre ⊢ O ∈ Fin ∧ A ⊆ O ∧ k ∈ O → 𝟙 O ⁡ A ⁡ k ∈ ℝ
4 3 recnd ⊢ O ∈ Fin ∧ A ⊆ O ∧ k ∈ O → 𝟙 O ⁡ A ⁡ k ∈ ℂ
5 4 mulridd ⊢ O ∈ Fin ∧ A ⊆ O ∧ k ∈ O → 𝟙 O ⁡ A ⁡ k ⋅ 1 = 𝟙 O ⁡ A ⁡ k
6 2 5 eqtr4id ⊢ O ∈ Fin ∧ A ⊆ O ∧ k ∈ O → 1 ˙ ⁡ k = 𝟙 O ⁡ A ⁡ k ⋅ 1
7 6 ralrimiva ⊢ O ∈ Fin ∧ A ⊆ O → ∀ k ∈ O 1 ˙ ⁡ k = 𝟙 O ⁡ A ⁡ k ⋅ 1
8 7 sumeq2d ⊢ O ∈ Fin ∧ A ⊆ O → ∑ k ∈ O 1 ˙ ⁡ k = ∑ k ∈ O 𝟙 O ⁡ A ⁡ k ⋅ 1
9 simpl ⊢ O ∈ Fin ∧ A ⊆ O → O ∈ Fin
10 simpr ⊢ O ∈ Fin ∧ A ⊆ O → A ⊆ O
11 1cnd ⊢ O ∈ Fin ∧ A ⊆ O ∧ k ∈ O → 1 ∈ ℂ
12 9 10 11 indsum ⊢ O ∈ Fin ∧ A ⊆ O → ∑ k ∈ O 𝟙 O ⁡ A ⁡ k ⋅ 1 = ∑ k ∈ A 1
13 ssfi ⊢ O ∈ Fin ∧ A ⊆ O → A ∈ Fin
14 fsumconst1 ⊢ A ∈ Fin → ∑ k ∈ A 1 = A
15 13 14 syl ⊢ O ∈ Fin ∧ A ⊆ O → ∑ k ∈ A 1 = A
16 8 12 15 3eqtrd ⊢ O ∈ Fin ∧ A ⊆ O → ∑ k ∈ O 1 ˙ ⁡ k = A