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. = ( ( _Ind ` O ) ` A )
Assertion indsumhash 
|- ( ( O e. Fin /\ A C_ O ) -> sum_ k e. O ( .1. ` k ) = ( # ` A ) )

Proof

Step Hyp Ref Expression
1 indsumhash.f 
 |-  .1. = ( ( _Ind ` O ) ` A )
2 1 fveq1i 
 |-  ( .1. ` k ) = ( ( ( _Ind ` O ) ` A ) ` k )
3 fvindre 
 |-  ( ( ( O e. Fin /\ A C_ O ) /\ k e. O ) -> ( ( ( _Ind ` O ) ` A ) ` k ) e. RR )
4 3 recnd 
 |-  ( ( ( O e. Fin /\ A C_ O ) /\ k e. O ) -> ( ( ( _Ind ` O ) ` A ) ` k ) e. CC )
5 4 mulridd 
 |-  ( ( ( O e. Fin /\ A C_ O ) /\ k e. O ) -> ( ( ( ( _Ind ` O ) ` A ) ` k ) x. 1 ) = ( ( ( _Ind ` O ) ` A ) ` k ) )
6 2 5 eqtr4id 
 |-  ( ( ( O e. Fin /\ A C_ O ) /\ k e. O ) -> ( .1. ` k ) = ( ( ( ( _Ind ` O ) ` A ) ` k ) x. 1 ) )
7 6 ralrimiva 
 |-  ( ( O e. Fin /\ A C_ O ) -> A. k e. O ( .1. ` k ) = ( ( ( ( _Ind ` O ) ` A ) ` k ) x. 1 ) )
8 7 sumeq2d 
 |-  ( ( O e. Fin /\ A C_ O ) -> sum_ k e. O ( .1. ` k ) = sum_ k e. O ( ( ( ( _Ind ` O ) ` A ) ` k ) x. 1 ) )
9 simpl 
 |-  ( ( O e. Fin /\ A C_ O ) -> O e. Fin )
10 simpr 
 |-  ( ( O e. Fin /\ A C_ O ) -> A C_ O )
11 1cnd 
 |-  ( ( ( O e. Fin /\ A C_ O ) /\ k e. O ) -> 1 e. CC )
12 9 10 11 indsum 
 |-  ( ( O e. Fin /\ A C_ O ) -> sum_ k e. O ( ( ( ( _Ind ` O ) ` A ) ` k ) x. 1 ) = sum_ k e. A 1 )
13 ssfi 
 |-  ( ( O e. Fin /\ A C_ O ) -> A e. Fin )
14 fsumconst1 
 |-  ( A e. Fin -> sum_ k e. A 1 = ( # ` A ) )
15 13 14 syl 
 |-  ( ( O e. Fin /\ A C_ O ) -> sum_ k e. A 1 = ( # ` A ) )
16 8 12 15 3eqtrd 
 |-  ( ( O e. Fin /\ A C_ O ) -> sum_ k e. O ( .1. ` k ) = ( # ` A ) )