Theorem reprval

Description: Value of the representations of M as the sum of S nonnegative integers in a given set A . (Contributed by Thierry Arnoux, 1-Dec-2021)

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

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		df-repr	|- repr = ( s e. NN0 |-> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m } ) )
5		oveq2	|- ( s = S -> ( 0 ..^ s ) = ( 0 ..^ S ) )
6	5	oveq2d	|- ( s = S -> ( b ^m ( 0 ..^ s ) ) = ( b ^m ( 0 ..^ S ) ) )
7	5	sumeq1d	|- ( s = S -> sum_ a e. ( 0 ..^ s ) ( c ` a ) = sum_ a e. ( 0 ..^ S ) ( c ` a ) )
8	7	eqeq1d	|- ( s = S -> ( sum_ a e. ( 0 ..^ s ) ( c ` a ) = m <-> sum_ a e. ( 0 ..^ S ) ( c ` a ) = m ) )
9	6 8	rabeqbidv	|- ( s = S -> { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m } = { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } )
10	9	mpoeq3dv	|- ( s = S -> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ s ) ) | sum_ a e. ( 0 ..^ s ) ( c ` a ) = m } ) = ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } ) )
11		nnex	|- NN e. _V
12	11	pwex	|- ~P NN e. _V
13		zex	|- ZZ e. _V
14	12 13	mpoex	|- ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } ) e. _V
15	14	a1i	|- ( ph -> ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } ) e. _V )
16	4 10 3 15	fvmptd3	|- ( ph -> ( repr ` S ) = ( b e. ~P NN , m e. ZZ |-> { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } ) )
17		simprl	|- ( ( ph /\ ( b = A /\ m = M ) ) -> b = A )
18	17	oveq1d	|- ( ( ph /\ ( b = A /\ m = M ) ) -> ( b ^m ( 0 ..^ S ) ) = ( A ^m ( 0 ..^ S ) ) )
19		simprr	|- ( ( ph /\ ( b = A /\ m = M ) ) -> m = M )
20	19	eqeq2d	|- ( ( ph /\ ( b = A /\ m = M ) ) -> ( sum_ a e. ( 0 ..^ S ) ( c ` a ) = m <-> sum_ a e. ( 0 ..^ S ) ( c ` a ) = M ) )
21	18 20	rabeqbidv	|- ( ( ph /\ ( b = A /\ m = M ) ) -> { c e. ( b ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = m } = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
22	11	a1i	|- ( ph -> NN e. _V )
23	22 1	ssexd	|- ( ph -> A e. _V )
24	23 1	elpwd	|- ( ph -> A e. ~P NN )
25		ovex	|- ( A ^m ( 0 ..^ S ) ) e. _V
26	25	rabex	|- { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } e. _V
27	26	a1i	|- ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } e. _V )
28	16 21 24 2 27	ovmpod	|- ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )