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 e. Fin /\ A C_ B ) -> sum_ k e. B if ( k e. A , 1 , 0 ) = ( # ` A ) )

Proof

Step Hyp Ref Expression
1 ssfi 
 |-  ( ( B e. Fin /\ A C_ B ) -> A e. Fin )
2 ax-1cn 
 |-  1 e. CC
3 fsumconst 
 |-  ( ( A e. Fin /\ 1 e. CC ) -> sum_ k e. A 1 = ( ( # ` A ) x. 1 ) )
4 1 2 3 sylancl 
 |-  ( ( B e. Fin /\ A C_ B ) -> sum_ k e. A 1 = ( ( # ` A ) x. 1 ) )
5 simpr 
 |-  ( ( B e. Fin /\ A C_ B ) -> A C_ B )
6 2 rgenw 
 |-  A. k e. A 1 e. CC
7 6 a1i 
 |-  ( ( B e. Fin /\ A C_ B ) -> A. k e. A 1 e. CC )
8 animorlr 
 |-  ( ( B e. Fin /\ A C_ B ) -> ( B C_ ( ZZ>= ` C ) \/ B e. Fin ) )
9 sumss2 
 |-  ( ( ( A C_ B /\ A. k e. A 1 e. CC ) /\ ( B C_ ( ZZ>= ` C ) \/ B e. Fin ) ) -> sum_ k e. A 1 = sum_ k e. B if ( k e. A , 1 , 0 ) )
10 5 7 8 9 syl21anc 
 |-  ( ( B e. Fin /\ A C_ B ) -> sum_ k e. A 1 = sum_ k e. B if ( k e. A , 1 , 0 ) )
11 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
12 1 11 syl 
 |-  ( ( B e. Fin /\ A C_ B ) -> ( # ` A ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( B e. Fin /\ A C_ B ) -> ( # ` A ) e. CC )
14 13 mulid1d 
 |-  ( ( B e. Fin /\ A C_ B ) -> ( ( # ` A ) x. 1 ) = ( # ` A ) )
15 4 10 14 3eqtr3d 
 |-  ( ( B e. Fin /\ A C_ B ) -> sum_ k e. B if ( k e. A , 1 , 0 ) = ( # ` A ) )