Metamath Proof Explorer

Theorem sticksstones9

Description: Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

Ref Expression
Hypotheses sticksstones9.1 
|- ( ph -> N e. NN0 )
sticksstones9.2 
|- ( ph -> K = 0 )
sticksstones9.3 
|- G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
sticksstones9.4 
|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
sticksstones9.5 
|- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion sticksstones9 
|- ( ph -> G : B --> A )

Proof

Step Hyp Ref Expression
1 sticksstones9.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones9.2 
 |-  ( ph -> K = 0 )
3 sticksstones9.3 
 |-  G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
4 sticksstones9.4 
 |-  A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
5 sticksstones9.5 
 |-  B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
6 2 iftrued 
 |-  ( ph -> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = { <. 1 , N >. } )
7 6 adantr 
 |-  ( ( ph /\ b e. B ) -> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) = { <. 1 , N >. } )
8 eqid 
 |-  { <. 1 , N >. } = { <. 1 , N >. }
9 1nn 
 |-  1 e. NN
10 9 a1i 
 |-  ( ph -> 1 e. NN )
11 fsng 
 |-  ( ( 1 e. NN /\ N e. NN0 ) -> ( { <. 1 , N >. } : { 1 } --> { N } <-> { <. 1 , N >. } = { <. 1 , N >. } ) )
12 10 1 11 syl2anc 
 |-  ( ph -> ( { <. 1 , N >. } : { 1 } --> { N } <-> { <. 1 , N >. } = { <. 1 , N >. } ) )
13 8 12 mpbiri 
 |-  ( ph -> { <. 1 , N >. } : { 1 } --> { N } )
14 1 snssd 
 |-  ( ph -> { N } C_ NN0 )
15 13 14 jca 
 |-  ( ph -> ( { <. 1 , N >. } : { 1 } --> { N } /\ { N } C_ NN0 ) )
16 fss 
 |-  ( ( { <. 1 , N >. } : { 1 } --> { N } /\ { N } C_ NN0 ) -> { <. 1 , N >. } : { 1 } --> NN0 )
17 15 16 syl 
 |-  ( ph -> { <. 1 , N >. } : { 1 } --> NN0 )
18 2 oveq1d 
 |-  ( ph -> ( K + 1 ) = ( 0 + 1 ) )
19 0p1e1 
 |-  ( 0 + 1 ) = 1
20 18 19 eqtrdi 
 |-  ( ph -> ( K + 1 ) = 1 )
21 20 oveq2d 
 |-  ( ph -> ( 1 ... ( K + 1 ) ) = ( 1 ... 1 ) )
22 1zzd 
 |-  ( ph -> 1 e. ZZ )
23 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
24 22 23 syl 
 |-  ( ph -> ( 1 ... 1 ) = { 1 } )
25 21 24 eqtrd 
 |-  ( ph -> ( 1 ... ( K + 1 ) ) = { 1 } )
26 25 eqcomd 
 |-  ( ph -> { 1 } = ( 1 ... ( K + 1 ) ) )
27 26 feq2d 
 |-  ( ph -> ( { <. 1 , N >. } : { 1 } --> NN0 <-> { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 ) )
28 17 27 mpbid 
 |-  ( ph -> { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 )
29 25 sumeq1d 
 |-  ( ph -> sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = sum_ i e. { 1 } ( { <. 1 , N >. } ` i ) )
30 fvsng 
 |-  ( ( 1 e. NN /\ N e. NN0 ) -> ( { <. 1 , N >. } ` 1 ) = N )
31 10 1 30 syl2anc 
 |-  ( ph -> ( { <. 1 , N >. } ` 1 ) = N )
32 1 nn0cnd 
 |-  ( ph -> N e. CC )
33 31 32 eqeltrd 
 |-  ( ph -> ( { <. 1 , N >. } ` 1 ) e. CC )
34 10 33 jca 
 |-  ( ph -> ( 1 e. NN /\ ( { <. 1 , N >. } ` 1 ) e. CC ) )
35 fveq2 
 |-  ( i = 1 -> ( { <. 1 , N >. } ` i ) = ( { <. 1 , N >. } ` 1 ) )
36 35 sumsn 
 |-  ( ( 1 e. NN /\ ( { <. 1 , N >. } ` 1 ) e. CC ) -> sum_ i e. { 1 } ( { <. 1 , N >. } ` i ) = ( { <. 1 , N >. } ` 1 ) )
37 34 36 syl 
 |-  ( ph -> sum_ i e. { 1 } ( { <. 1 , N >. } ` i ) = ( { <. 1 , N >. } ` 1 ) )
38 10 1 jca 
 |-  ( ph -> ( 1 e. NN /\ N e. NN0 ) )
39 38 30 syl 
 |-  ( ph -> ( { <. 1 , N >. } ` 1 ) = N )
40 37 39 eqtrd 
 |-  ( ph -> sum_ i e. { 1 } ( { <. 1 , N >. } ` i ) = N )
41 29 40 eqtrd 
 |-  ( ph -> sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N )
42 28 41 jca 
 |-  ( ph -> ( { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) )
43 42 adantr 
 |-  ( ( ph /\ b e. B ) -> ( { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) )
44 snex 
 |-  { <. 1 , N >. } e. _V
45 feq1 
 |-  ( g = { <. 1 , N >. } -> ( g : ( 1 ... ( K + 1 ) ) --> NN0 <-> { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 ) )
46 simpl 
 |-  ( ( g = { <. 1 , N >. } /\ i e. ( 1 ... ( K + 1 ) ) ) -> g = { <. 1 , N >. } )
47 46 fveq1d 
 |-  ( ( g = { <. 1 , N >. } /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( g ` i ) = ( { <. 1 , N >. } ` i ) )
48 47 sumeq2dv 
 |-  ( g = { <. 1 , N >. } -> sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) )
49 48 eqeq1d 
 |-  ( g = { <. 1 , N >. } -> ( sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N <-> sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) )
50 45 49 anbi12d 
 |-  ( g = { <. 1 , N >. } -> ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) <-> ( { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) ) )
51 50 elabg 
 |-  ( { <. 1 , N >. } e. _V -> ( { <. 1 , N >. } e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) ) )
52 44 51 ax-mp 
 |-  ( { <. 1 , N >. } e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( { <. 1 , N >. } : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( { <. 1 , N >. } ` i ) = N ) )
53 43 52 sylibr 
 |-  ( ( ph /\ b e. B ) -> { <. 1 , N >. } e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
54 4 a1i 
 |-  ( ( ph /\ b e. B ) -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
55 53 54 eleqtrrd 
 |-  ( ( ph /\ b e. B ) -> { <. 1 , N >. } e. A )
56 7 55 eqeltrd 
 |-  ( ( ph /\ b e. B ) -> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) e. A )
57 56 3 fmptd 
 |-  ( ph -> G : B --> A )