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

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 = ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 )
Assertion indsumhash ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → Σ 𝑘 ∈ 𝑂 ( 1 ‘ 𝑘 ) = ( ♯ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 indsumhash.f ⊢ 1 = ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 )
2 1 fveq1i ⊢ ( 1 ‘ 𝑘 ) = ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 )
3 fvindre ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑘 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
4 3 recnd ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑘 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) ∈ ℂ )
5 4 mulridd ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑘 ∈ 𝑂 ) → ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) · 1 ) = ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) )
6 2 5 eqtr4id ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑘 ∈ 𝑂 ) → ( 1 ‘ 𝑘 ) = ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) · 1 ) )
7 6 ralrimiva ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → ∀ 𝑘 ∈ 𝑂 ( 1 ‘ 𝑘 ) = ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) · 1 ) )
8 7 sumeq2d ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → Σ 𝑘 ∈ 𝑂 ( 1 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) · 1 ) )
9 simpl ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → 𝑂 ∈ Fin )
10 simpr ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ⊆ 𝑂 )
11 1cnd ⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑘 ∈ 𝑂 ) → 1 ∈ ℂ )
12 9 10 11 indsum ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → Σ 𝑘 ∈ 𝑂 ( ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑘 ) · 1 ) = Σ 𝑘 ∈ 𝐴 1 )
13 ssfi ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → 𝐴 ∈ Fin )
14 fsumconst1 ⊢ ( 𝐴 ∈ Fin → Σ 𝑘 ∈ 𝐴 1 = ( ♯ ‘ 𝐴 ) )
15 13 14 syl ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → Σ 𝑘 ∈ 𝐴 1 = ( ♯ ‘ 𝐴 ) )
16 8 12 15 3eqtrd ⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → Σ 𝑘 ∈ 𝑂 ( 1 ‘ 𝑘 ) = ( ♯ ‘ 𝐴 ) )