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

Metamath Proof Explorer

Theorem reprsum

Description: Sums of values of the members of the representation of M equal M . (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 reprsum 
|- ( ph -> 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 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 fveq1 
 |-  ( c = C -> ( c ` a ) = ( C ` a ) )
8 7 sumeq2sdv 
 |-  ( c = C -> sum_ a e. ( 0 ..^ S ) ( c ` a ) = sum_ a e. ( 0 ..^ S ) ( C ` a ) )
9 8 eqeq1d 
 |-  ( c = C -> ( sum_ a e. ( 0 ..^ S ) ( c ` a ) = M <-> sum_ a e. ( 0 ..^ S ) ( C ` a ) = M ) )
10 9 elrab 
 |-  ( C e. { c e. ( A ^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 ) )
11 6 10 sylib 
 |-  ( ph -> ( C e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( C ` a ) = M ) )
12 11 simprd 
 |-  ( ph -> sum_ a e. ( 0 ..^ S ) ( C ` a ) = M )