Metamath Proof Explorer

Theorem hashbc

Description: The binomial coefficient counts the number of subsets of a finite set of a given size. This is Metamath 100 proof #58 (formula for the number of combinations). (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion hashbc 
|- ( ( A e. Fin /\ K e. ZZ ) -> ( ( # ` A ) _C K ) = ( # ` { x e. ~P A | ( # ` x ) = K } ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( w = (/) -> ( # ` w ) = ( # ` (/) ) )
2 1 oveq1d 
 |-  ( w = (/) -> ( ( # ` w ) _C k ) = ( ( # ` (/) ) _C k ) )
3 pweq 
 |-  ( w = (/) -> ~P w = ~P (/) )
4 3 rabeqdv 
 |-  ( w = (/) -> { x e. ~P w | ( # ` x ) = k } = { x e. ~P (/) | ( # ` x ) = k } )
5 4 fveq2d 
 |-  ( w = (/) -> ( # ` { x e. ~P w | ( # ` x ) = k } ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
6 2 5 eqeq12d 
 |-  ( w = (/) -> ( ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) ) )
7 6 ralbidv 
 |-  ( w = (/) -> ( A. k e. ZZ ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> A. k e. ZZ ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) ) )
8 fveq2 
 |-  ( w = y -> ( # ` w ) = ( # ` y ) )
9 8 oveq1d 
 |-  ( w = y -> ( ( # ` w ) _C k ) = ( ( # ` y ) _C k ) )
10 pweq 
 |-  ( w = y -> ~P w = ~P y )
11 10 rabeqdv 
 |-  ( w = y -> { x e. ~P w | ( # ` x ) = k } = { x e. ~P y | ( # ` x ) = k } )
12 11 fveq2d 
 |-  ( w = y -> ( # ` { x e. ~P w | ( # ` x ) = k } ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) )
13 9 12 eqeq12d 
 |-  ( w = y -> ( ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> ( ( # ` y ) _C k ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) ) )
14 13 ralbidv 
 |-  ( w = y -> ( A. k e. ZZ ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> A. k e. ZZ ( ( # ` y ) _C k ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) ) )
15 fveq2 
 |-  ( w = ( y u. { z } ) -> ( # ` w ) = ( # ` ( y u. { z } ) ) )
16 15 oveq1d 
 |-  ( w = ( y u. { z } ) -> ( ( # ` w ) _C k ) = ( ( # ` ( y u. { z } ) ) _C k ) )
17 pweq 
 |-  ( w = ( y u. { z } ) -> ~P w = ~P ( y u. { z } ) )
18 17 rabeqdv 
 |-  ( w = ( y u. { z } ) -> { x e. ~P w | ( # ` x ) = k } = { x e. ~P ( y u. { z } ) | ( # ` x ) = k } )
19 18 fveq2d 
 |-  ( w = ( y u. { z } ) -> ( # ` { x e. ~P w | ( # ` x ) = k } ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) )
20 16 19 eqeq12d 
 |-  ( w = ( y u. { z } ) -> ( ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) ) )
21 20 ralbidv 
 |-  ( w = ( y u. { z } ) -> ( A. k e. ZZ ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> A. k e. ZZ ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) ) )
22 fveq2 
 |-  ( w = A -> ( # ` w ) = ( # ` A ) )
23 22 oveq1d 
 |-  ( w = A -> ( ( # ` w ) _C k ) = ( ( # ` A ) _C k ) )
24 pweq 
 |-  ( w = A -> ~P w = ~P A )
25 24 rabeqdv 
 |-  ( w = A -> { x e. ~P w | ( # ` x ) = k } = { x e. ~P A | ( # ` x ) = k } )
26 25 fveq2d 
 |-  ( w = A -> ( # ` { x e. ~P w | ( # ` x ) = k } ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) )
27 23 26 eqeq12d 
 |-  ( w = A -> ( ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> ( ( # ` A ) _C k ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) ) )
28 27 ralbidv 
 |-  ( w = A -> ( A. k e. ZZ ( ( # ` w ) _C k ) = ( # ` { x e. ~P w | ( # ` x ) = k } ) <-> A. k e. ZZ ( ( # ` A ) _C k ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) ) )
29 hash0 
 |-  ( # ` (/) ) = 0
30 29 a1i 
 |-  ( k e. ( 0 ... 0 ) -> ( # ` (/) ) = 0 )
31 elfz1eq 
 |-  ( k e. ( 0 ... 0 ) -> k = 0 )
32 30 31 oveq12d 
 |-  ( k e. ( 0 ... 0 ) -> ( ( # ` (/) ) _C k ) = ( 0 _C 0 ) )
33 0nn0 
 |-  0 e. NN0
34 bcn0 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
35 33 34 ax-mp 
 |-  ( 0 _C 0 ) = 1
36 32 35 eqtrdi 
 |-  ( k e. ( 0 ... 0 ) -> ( ( # ` (/) ) _C k ) = 1 )
37 pw0 
 |-  ~P (/) = { (/) }
38 31 eqcomd 
 |-  ( k e. ( 0 ... 0 ) -> 0 = k )
39 37 raleqi 
 |-  ( A. x e. ~P (/) ( # ` x ) = k <-> A. x e. { (/) } ( # ` x ) = k )
40 0ex 
 |-  (/) e. _V
41 fveq2 
 |-  ( x = (/) -> ( # ` x ) = ( # ` (/) ) )
42 41 29 eqtrdi 
 |-  ( x = (/) -> ( # ` x ) = 0 )
43 42 eqeq1d 
 |-  ( x = (/) -> ( ( # ` x ) = k <-> 0 = k ) )
44 40 43 ralsn 
 |-  ( A. x e. { (/) } ( # ` x ) = k <-> 0 = k )
45 39 44 bitri 
 |-  ( A. x e. ~P (/) ( # ` x ) = k <-> 0 = k )
46 38 45 sylibr 
 |-  ( k e. ( 0 ... 0 ) -> A. x e. ~P (/) ( # ` x ) = k )
47 rabid2 
 |-  ( ~P (/) = { x e. ~P (/) | ( # ` x ) = k } <-> A. x e. ~P (/) ( # ` x ) = k )
48 46 47 sylibr 
 |-  ( k e. ( 0 ... 0 ) -> ~P (/) = { x e. ~P (/) | ( # ` x ) = k } )
49 37 48 syl5reqr 
 |-  ( k e. ( 0 ... 0 ) -> { x e. ~P (/) | ( # ` x ) = k } = { (/) } )
50 49 fveq2d 
 |-  ( k e. ( 0 ... 0 ) -> ( # ` { x e. ~P (/) | ( # ` x ) = k } ) = ( # ` { (/) } ) )
51 hashsng 
 |-  ( (/) e. _V -> ( # ` { (/) } ) = 1 )
52 40 51 ax-mp 
 |-  ( # ` { (/) } ) = 1
53 50 52 eqtrdi 
 |-  ( k e. ( 0 ... 0 ) -> ( # ` { x e. ~P (/) | ( # ` x ) = k } ) = 1 )
54 36 53 eqtr4d 
 |-  ( k e. ( 0 ... 0 ) -> ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
55 54 adantl 
 |-  ( ( k e. ZZ /\ k e. ( 0 ... 0 ) ) -> ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
56 29 oveq1i 
 |-  ( ( # ` (/) ) _C k ) = ( 0 _C k )
57 bcval3 
 |-  ( ( 0 e. NN0 /\ k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) = 0 )
58 33 57 mp3an1 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) = 0 )
59 id 
 |-  ( 0 = k -> 0 = k )
60 0z 
 |-  0 e. ZZ
61 elfz3 
 |-  ( 0 e. ZZ -> 0 e. ( 0 ... 0 ) )
62 60 61 ax-mp 
 |-  0 e. ( 0 ... 0 )
63 59 62 eqeltrrdi 
 |-  ( 0 = k -> k e. ( 0 ... 0 ) )
64 63 con3i 
 |-  ( -. k e. ( 0 ... 0 ) -> -. 0 = k )
65 64 adantl 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> -. 0 = k )
66 37 raleqi 
 |-  ( A. x e. ~P (/) -. ( # ` x ) = k <-> A. x e. { (/) } -. ( # ` x ) = k )
67 43 notbid 
 |-  ( x = (/) -> ( -. ( # ` x ) = k <-> -. 0 = k ) )
68 40 67 ralsn 
 |-  ( A. x e. { (/) } -. ( # ` x ) = k <-> -. 0 = k )
69 66 68 bitri 
 |-  ( A. x e. ~P (/) -. ( # ` x ) = k <-> -. 0 = k )
70 65 69 sylibr 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> A. x e. ~P (/) -. ( # ` x ) = k )
71 rabeq0 
 |-  ( { x e. ~P (/) | ( # ` x ) = k } = (/) <-> A. x e. ~P (/) -. ( # ` x ) = k )
72 70 71 sylibr 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> { x e. ~P (/) | ( # ` x ) = k } = (/) )
73 72 fveq2d 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( # ` { x e. ~P (/) | ( # ` x ) = k } ) = ( # ` (/) ) )
74 73 29 eqtrdi 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( # ` { x e. ~P (/) | ( # ` x ) = k } ) = 0 )
75 58 74 eqtr4d 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( 0 _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
76 56 75 syl5eq 
 |-  ( ( k e. ZZ /\ -. k e. ( 0 ... 0 ) ) -> ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
77 55 76 pm2.61dan 
 |-  ( k e. ZZ -> ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } ) )
78 77 rgen 
 |-  A. k e. ZZ ( ( # ` (/) ) _C k ) = ( # ` { x e. ~P (/) | ( # ` x ) = k } )
79 oveq2 
 |-  ( k = j -> ( ( # ` y ) _C k ) = ( ( # ` y ) _C j ) )
80 eqeq2 
 |-  ( k = j -> ( ( # ` x ) = k <-> ( # ` x ) = j ) )
81 80 rabbidv 
 |-  ( k = j -> { x e. ~P y | ( # ` x ) = k } = { x e. ~P y | ( # ` x ) = j } )
82 fveqeq2 
 |-  ( x = z -> ( ( # ` x ) = j <-> ( # ` z ) = j ) )
83 82 cbvrabv 
 |-  { x e. ~P y | ( # ` x ) = j } = { z e. ~P y | ( # ` z ) = j }
84 81 83 eqtrdi 
 |-  ( k = j -> { x e. ~P y | ( # ` x ) = k } = { z e. ~P y | ( # ` z ) = j } )
85 84 fveq2d 
 |-  ( k = j -> ( # ` { x e. ~P y | ( # ` x ) = k } ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) )
86 79 85 eqeq12d 
 |-  ( k = j -> ( ( ( # ` y ) _C k ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) <-> ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) )
87 86 cbvralvw 
 |-  ( A. k e. ZZ ( ( # ` y ) _C k ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) <-> A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) )
88 simpll 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> y e. Fin )
89 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> -. z e. y )
90 simprr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) )
91 83 fveq2i 
 |-  ( # ` { x e. ~P y | ( # ` x ) = j } ) = ( # ` { z e. ~P y | ( # ` z ) = j } )
92 91 eqeq2i 
 |-  ( ( ( # ` y ) _C j ) = ( # ` { x e. ~P y | ( # ` x ) = j } ) <-> ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) )
93 92 ralbii 
 |-  ( A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { x e. ~P y | ( # ` x ) = j } ) <-> A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) )
94 90 93 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { x e. ~P y | ( # ` x ) = j } ) )
95 simprl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> k e. ZZ )
96 88 89 94 95 hashbclem 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( k e. ZZ /\ A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) ) ) -> ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) )
97 96 expr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ k e. ZZ ) -> ( A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) -> ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) ) )
98 97 ralrimdva 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. j e. ZZ ( ( # ` y ) _C j ) = ( # ` { z e. ~P y | ( # ` z ) = j } ) -> A. k e. ZZ ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) ) )
99 87 98 syl5bi 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( A. k e. ZZ ( ( # ` y ) _C k ) = ( # ` { x e. ~P y | ( # ` x ) = k } ) -> A. k e. ZZ ( ( # ` ( y u. { z } ) ) _C k ) = ( # ` { x e. ~P ( y u. { z } ) | ( # ` x ) = k } ) ) )
100 7 14 21 28 78 99 findcard2s 
 |-  ( A e. Fin -> A. k e. ZZ ( ( # ` A ) _C k ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) )
101 oveq2 
 |-  ( k = K -> ( ( # ` A ) _C k ) = ( ( # ` A ) _C K ) )
102 eqeq2 
 |-  ( k = K -> ( ( # ` x ) = k <-> ( # ` x ) = K ) )
103 102 rabbidv 
 |-  ( k = K -> { x e. ~P A | ( # ` x ) = k } = { x e. ~P A | ( # ` x ) = K } )
104 103 fveq2d 
 |-  ( k = K -> ( # ` { x e. ~P A | ( # ` x ) = k } ) = ( # ` { x e. ~P A | ( # ` x ) = K } ) )
105 101 104 eqeq12d 
 |-  ( k = K -> ( ( ( # ` A ) _C k ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) <-> ( ( # ` A ) _C K ) = ( # ` { x e. ~P A | ( # ` x ) = K } ) ) )
106 105 rspccva 
 |-  ( ( A. k e. ZZ ( ( # ` A ) _C k ) = ( # ` { x e. ~P A | ( # ` x ) = k } ) /\ K e. ZZ ) -> ( ( # ` A ) _C K ) = ( # ` { x e. ~P A | ( # ` x ) = K } ) )
107 100 106 sylan 
 |-  ( ( A e. Fin /\ K e. ZZ ) -> ( ( # ` A ) _C K ) = ( # ` { x e. ~P A | ( # ` x ) = K } ) )