This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )