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 )