Theorem reprf

Description: Members of the representation of M as the sum of S nonnegative integers from set A as functions. (Contributed by Thierry Arnoux, 5-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	|- ( ph -> A C_ NN )
	reprval.m	|- ( ph -> M e. ZZ )
	reprval.s	|- ( ph -> S e. NN0 )
	reprf.c	|- ( ph -> C e. ( A ( repr ` S ) M ) )
Assertion	reprf	|- ( ph -> C : ( 0 ..^ S ) --> A )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	|- ( ph -> A C_ NN )
2		reprval.m	|- ( ph -> M e. ZZ )
3		reprval.s	|- ( ph -> S e. NN0 )
4		reprf.c	|- ( ph -> C e. ( A ( repr ` S ) M ) )
5	1 2 3	reprval	|- ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
6	4 5	eleqtrd	|- ( ph -> C e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
7		elrabi	|- ( C e. { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } -> C e. ( A ^m ( 0 ..^ S ) ) )
8		elmapi	|- ( C e. ( A ^m ( 0 ..^ S ) ) -> C : ( 0 ..^ S ) --> A )
9	6 7 8	3syl	|- ( ph -> C : ( 0 ..^ S ) --> A )