reprsum

Description: Sums of values of the members of the representation of M equal M . (Contributed by Thierry Arnoux, 5-Dec-2021)

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		reprf.c	$⊢ φ \to C \in (A repr (S) M)$
5	1 2 3	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
6	4 5	eleqtrd	$⊢ φ \to C \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
7		fveq1	$⊢ c = C \to c (a) = C (a)$
8	7	sumeq2sdv	$⊢ c = C \to \sum_{a \in (0 ..^S)} c (a) = \sum_{a \in (0 ..^S)} C (a)$
9	8	eqeq1d	$⊢ c = C \to (\sum_{a \in (0 ..^S)} c (a) = M \leftrightarrow \sum_{a \in (0 ..^S)} C (a) = M)$
10	9	elrab	$⊢ C \in \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \leftrightarrow (C \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} C (a) = M)$
11	6 10	sylib	$⊢ φ \to (C \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} C (a) = M)$
12	11	simprd	$⊢ φ \to \sum_{a \in (0 ..^S)} C (a) = M$

Metamath Proof Explorer