Theorem hashrepr

Description: Develop the number of representations of an integer M as a sum of nonnegative integers in set A . (Contributed by Thierry Arnoux, 14-Dec-2021)

	Ref	Expression
Hypotheses	hashrepr.a	|- ( ph -> A C_ NN )
	hashrepr.m	|- ( ph -> M e. NN0 )
	hashrepr.s	|- ( ph -> S e. NN0 )
Assertion	hashrepr	|- ( ph -> ( # ` ( A ( repr ` S ) M ) ) = sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )

Proof

Step	Hyp	Ref	Expression
1		hashrepr.a	|- ( ph -> A C_ NN )
2		hashrepr.m	|- ( ph -> M e. NN0 )
3		hashrepr.s	|- ( ph -> S e. NN0 )
4	2	nn0zd	|- ( ph -> M e. ZZ )
5		fzfid	|- ( ph -> ( 1 ... M ) e. Fin )
6		fz1ssnn	|- ( 1 ... M ) C_ NN
7	6	a1i	|- ( ph -> ( 1 ... M ) C_ NN )
8	1 4 3 5 7	hashreprin	|- ( ph -> ( # ` ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) ) = sum_ c e. ( ( 1 ... M ) ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
9	2 3 1	reprinfz1	|- ( ph -> ( A ( repr ` S ) M ) = ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) )
10	9	fveq2d	|- ( ph -> ( # ` ( A ( repr ` S ) M ) ) = ( # ` ( ( A i^i ( 1 ... M ) ) ( repr ` S ) M ) ) )
11	2 3	reprfz1	|- ( ph -> ( NN ( repr ` S ) M ) = ( ( 1 ... M ) ( repr ` S ) M ) )
12	11	sumeq1d	|- ( ph -> sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) = sum_ c e. ( ( 1 ... M ) ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
13	8 10 12	3eqtr4d	|- ( ph -> ( # ` ( A ( repr ` S ) M ) ) = sum_ c e. ( NN ( repr ` S ) M ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )