Metamath Proof Explorer

Theorem sticksstones17

Description: Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024)

Ref Expression
Hypotheses sticksstones17.1 
|- ( ph -> N e. NN0 )
sticksstones17.2 
|- ( ph -> K e. NN0 )
sticksstones17.3 
|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
sticksstones17.4 
|- B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
sticksstones17.5 
|- ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
sticksstones17.6 
|- G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
Assertion sticksstones17 
|- ( ph -> G : B --> A )

Proof

Step Hyp Ref Expression
1 sticksstones17.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones17.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones17.3 
 |-  A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
4 sticksstones17.4 
 |-  B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
5 sticksstones17.5 
 |-  ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
6 sticksstones17.6 
 |-  G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
7 4 eqimssi 
 |-  B C_ { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
8 7 a1i 
 |-  ( ph -> B C_ { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
9 8 sseld 
 |-  ( ph -> ( b e. B -> b e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } ) )
10 9 imp 
 |-  ( ( ph /\ b e. B ) -> b e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
11 vex 
 |-  b e. _V
12 feq1 
 |-  ( h = b -> ( h : S --> NN0 <-> b : S --> NN0 ) )
13 simpl 
 |-  ( ( h = b /\ i e. S ) -> h = b )
14 13 fveq1d 
 |-  ( ( h = b /\ i e. S ) -> ( h ` i ) = ( b ` i ) )
15 14 sumeq2dv 
 |-  ( h = b -> sum_ i e. S ( h ` i ) = sum_ i e. S ( b ` i ) )
16 15 eqeq1d 
 |-  ( h = b -> ( sum_ i e. S ( h ` i ) = N <-> sum_ i e. S ( b ` i ) = N ) )
17 12 16 anbi12d 
 |-  ( h = b -> ( ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) <-> ( b : S --> NN0 /\ sum_ i e. S ( b ` i ) = N ) ) )
18 11 17 elab 
 |-  ( b e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } <-> ( b : S --> NN0 /\ sum_ i e. S ( b ` i ) = N ) )
19 10 18 sylib 
 |-  ( ( ph /\ b e. B ) -> ( b : S --> NN0 /\ sum_ i e. S ( b ` i ) = N ) )
20 19 simpld 
 |-  ( ( ph /\ b e. B ) -> b : S --> NN0 )
21 20 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... K ) ) -> b : S --> NN0 )
22 21 3impa 
 |-  ( ( ph /\ b e. B /\ y e. ( 1 ... K ) ) -> b : S --> NN0 )
23 f1of 
 |-  ( Z : ( 1 ... K ) -1-1-onto-> S -> Z : ( 1 ... K ) --> S )
24 5 23 syl 
 |-  ( ph -> Z : ( 1 ... K ) --> S )
25 24 adantr 
 |-  ( ( ph /\ b e. B ) -> Z : ( 1 ... K ) --> S )
26 25 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... K ) ) -> Z : ( 1 ... K ) --> S )
27 26 3impa 
 |-  ( ( ph /\ b e. B /\ y e. ( 1 ... K ) ) -> Z : ( 1 ... K ) --> S )
28 simp3 
 |-  ( ( ph /\ b e. B /\ y e. ( 1 ... K ) ) -> y e. ( 1 ... K ) )
29 27 28 ffvelrnd 
 |-  ( ( ph /\ b e. B /\ y e. ( 1 ... K ) ) -> ( Z ` y ) e. S )
30 22 29 ffvelrnd 
 |-  ( ( ph /\ b e. B /\ y e. ( 1 ... K ) ) -> ( b ` ( Z ` y ) ) e. NN0 )
31 30 3expa 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... K ) ) -> ( b ` ( Z ` y ) ) e. NN0 )
32 31 fmpttd 
 |-  ( ( ph /\ b e. B ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 )
33 eqidd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
34 simpr 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ y = i ) -> y = i )
35 34 fveq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ y = i ) -> ( Z ` y ) = ( Z ` i ) )
36 35 fveq2d 
 |-  ( ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) /\ y = i ) -> ( b ` ( Z ` y ) ) = ( b ` ( Z ` i ) ) )
37 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> i e. ( 1 ... K ) )
38 fvexd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( b ` ( Z ` i ) ) e. _V )
39 33 36 37 38 fvmptd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = ( b ` ( Z ` i ) ) )
40 39 sumeq2dv 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = sum_ i e. ( 1 ... K ) ( b ` ( Z ` i ) ) )
41 fveq2 
 |-  ( s = ( Z ` i ) -> ( b ` s ) = ( b ` ( Z ` i ) ) )
42 fzfi 
 |-  ( 1 ... K ) e. Fin
43 42 a1i 
 |-  ( ( ph /\ b e. B ) -> ( 1 ... K ) e. Fin )
44 5 adantr 
 |-  ( ( ph /\ b e. B ) -> Z : ( 1 ... K ) -1-1-onto-> S )
45 eqidd 
 |-  ( ( ( ph /\ b e. B ) /\ i e. ( 1 ... K ) ) -> ( Z ` i ) = ( Z ` i ) )
46 nn0sscn 
 |-  NN0 C_ CC
47 46 a1i 
 |-  ( ( ph /\ b e. B ) -> NN0 C_ CC )
48 fss 
 |-  ( ( b : S --> NN0 /\ NN0 C_ CC ) -> b : S --> CC )
49 20 47 48 syl2anc 
 |-  ( ( ph /\ b e. B ) -> b : S --> CC )
50 49 ffvelrnda 
 |-  ( ( ( ph /\ b e. B ) /\ s e. S ) -> ( b ` s ) e. CC )
51 41 43 44 45 50 fsumf1o 
 |-  ( ( ph /\ b e. B ) -> sum_ s e. S ( b ` s ) = sum_ i e. ( 1 ... K ) ( b ` ( Z ` i ) ) )
52 51 eqcomd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( b ` ( Z ` i ) ) = sum_ s e. S ( b ` s ) )
53 fveq2 
 |-  ( s = i -> ( b ` s ) = ( b ` i ) )
54 53 cbvsumv 
 |-  sum_ s e. S ( b ` s ) = sum_ i e. S ( b ` i )
55 54 a1i 
 |-  ( ( ph /\ b e. B ) -> sum_ s e. S ( b ` s ) = sum_ i e. S ( b ` i ) )
56 19 simprd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. S ( b ` i ) = N )
57 55 56 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ s e. S ( b ` s ) = N )
58 52 57 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( b ` ( Z ` i ) ) = N )
59 40 58 eqtrd 
 |-  ( ( ph /\ b e. B ) -> sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N )
60 32 59 jca 
 |-  ( ( ph /\ b e. B ) -> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N ) )
61 fzfid 
 |-  ( ( ph /\ b e. B ) -> ( 1 ... K ) e. Fin )
62 61 mptexd 
 |-  ( ( ph /\ b e. B ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. _V )
63 feq1 
 |-  ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) -> ( g : ( 1 ... K ) --> NN0 <-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 ) )
64 simpl 
 |-  ( ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) /\ i e. ( 1 ... K ) ) -> g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
65 64 fveq1d 
 |-  ( ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) /\ i e. ( 1 ... K ) ) -> ( g ` i ) = ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) )
66 65 sumeq2dv 
 |-  ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) -> sum_ i e. ( 1 ... K ) ( g ` i ) = sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) )
67 66 eqeq1d 
 |-  ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) -> ( sum_ i e. ( 1 ... K ) ( g ` i ) = N <-> sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N ) )
68 63 67 anbi12d 
 |-  ( g = ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) -> ( ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) <-> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N ) ) )
69 68 elabg 
 |-  ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. _V -> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } <-> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N ) ) )
70 62 69 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } <-> ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ` i ) = N ) ) )
71 60 70 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
72 3 a1i 
 |-  ( ( ph /\ b e. B ) -> A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
73 71 72 eleqtrrd 
 |-  ( ( ph /\ b e. B ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) e. A )
74 73 6 fmptd 
 |-  ( ph -> G : B --> A )