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 ‘ 𝑘 ) = ( ♯ ‘ 𝐴 ) )