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

Metamath Proof Explorer

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 )