Metamath Proof Explorer

Theorem sticksstones21

Description: Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024)

Ref Expression
Hypotheses sticksstones21.1 
|- ( ph -> N e. NN0 )
sticksstones21.2 
|- ( ph -> S e. Fin )
sticksstones21.3 
|- ( ph -> S =/= (/) )
sticksstones21.4 
|- A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = N ) }
Assertion sticksstones21 
|- ( ph -> ( # ` A ) = ( ( N + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones21.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones21.2 
 |-  ( ph -> S e. Fin )
3 sticksstones21.3 
 |-  ( ph -> S =/= (/) )
4 sticksstones21.4 
 |-  A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = N ) }
5 hashnncl 
 |-  ( S e. Fin -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
6 2 5 syl 
 |-  ( ph -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
7 3 6 mpbird 
 |-  ( ph -> ( # ` S ) e. NN )
8 fveq2 
 |-  ( j = k -> ( g ` j ) = ( g ` k ) )
9 8 cbvsumv 
 |-  sum_ j e. ( 1 ... ( # ` S ) ) ( g ` j ) = sum_ k e. ( 1 ... ( # ` S ) ) ( g ` k )
10 9 eqeq1i 
 |-  ( sum_ j e. ( 1 ... ( # ` S ) ) ( g ` j ) = N <-> sum_ k e. ( 1 ... ( # ` S ) ) ( g ` k ) = N )
11 10 anbi2i 
 |-  ( ( g : ( 1 ... ( # ` S ) ) --> NN0 /\ sum_ j e. ( 1 ... ( # ` S ) ) ( g ` j ) = N ) <-> ( g : ( 1 ... ( # ` S ) ) --> NN0 /\ sum_ k e. ( 1 ... ( # ` S ) ) ( g ` k ) = N ) )
12 11 abbii 
 |-  { g | ( g : ( 1 ... ( # ` S ) ) --> NN0 /\ sum_ j e. ( 1 ... ( # ` S ) ) ( g ` j ) = N ) } = { g | ( g : ( 1 ... ( # ` S ) ) --> NN0 /\ sum_ k e. ( 1 ... ( # ` S ) ) ( g ` k ) = N ) }
13 fveq2 
 |-  ( i = k -> ( f ` i ) = ( f ` k ) )
14 13 cbvsumv 
 |-  sum_ i e. S ( f ` i ) = sum_ k e. S ( f ` k )
15 14 eqeq1i 
 |-  ( sum_ i e. S ( f ` i ) = N <-> sum_ k e. S ( f ` k ) = N )
16 15 anbi2i 
 |-  ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = N ) <-> ( f : S --> NN0 /\ sum_ k e. S ( f ` k ) = N ) )
17 16 abbii 
 |-  { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = N ) } = { f | ( f : S --> NN0 /\ sum_ k e. S ( f ` k ) = N ) }
18 4 17 eqtri 
 |-  A = { f | ( f : S --> NN0 /\ sum_ k e. S ( f ` k ) = N ) }
19 eqidd 
 |-  ( ph -> ( # ` S ) = ( # ` S ) )
20 1 2 7 12 18 19 sticksstones20 
 |-  ( ph -> ( # ` A ) = ( ( N + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) )