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	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
Assertion	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		df-repr	$⊢ repr = (s \in ℕ_{0} ⟼ (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^s)}) \| \sum_{a \in (0 ..^s)} c (a) = m\}))$
5		oveq2	$⊢ s = S \to (0 ..^s) = (0 ..^S)$
6	5	oveq2d	$⊢ s = S \to b^{(0 ..^s)} = b^{(0 ..^S)}$
7	5	sumeq1d	$⊢ s = S \to \sum_{a \in (0 ..^s)} c (a) = \sum_{a \in (0 ..^S)} c (a)$
8	7	eqeq1d	$⊢ s = S \to (\sum_{a \in (0 ..^s)} c (a) = m \leftrightarrow \sum_{a \in (0 ..^S)} c (a) = m)$
9	6 8	rabeqbidv	$⊢ s = S \to \{c \in (b^{(0 ..^s)}) \| \sum_{a \in (0 ..^s)} c (a) = m\} = \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\}$
10	9	mpoeq3dv	$⊢ s = S \to (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^s)}) \| \sum_{a \in (0 ..^s)} c (a) = m\}) = (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\})$
11		nnex	$⊢ ℕ \in V$
12	11	pwex	$⊢ 𝒫 ℕ \in V$
13		zex	$⊢ ℤ \in V$
14	12 13	mpoex	$⊢ (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\}) \in V$
15	14	a1i	$⊢ φ \to (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\}) \in V$
16	4 10 3 15	fvmptd3	$⊢ φ \to repr (S) = (b \in 𝒫 ℕ, m \in ℤ ⟼ \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\})$
17		simprl	$⊢ (φ \land (b = A \land m = M)) \to b = A$
18	17	oveq1d	$⊢ (φ \land (b = A \land m = M)) \to b^{(0 ..^S)} = A^{(0 ..^S)}$
19		simprr	$⊢ (φ \land (b = A \land m = M)) \to m = M$
20	19	eqeq2d	$⊢ (φ \land (b = A \land m = M)) \to (\sum_{a \in (0 ..^S)} c (a) = m \leftrightarrow \sum_{a \in (0 ..^S)} c (a) = M)$
21	18 20	rabeqbidv	$⊢ (φ \land (b = A \land m = M)) \to \{c \in (b^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = m\} = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
22	11	a1i	$⊢ φ \to ℕ \in V$
23	22 1	ssexd	$⊢ φ \to A \in V$
24	23 1	elpwd	$⊢ φ \to A \in 𝒫 ℕ$
25		ovex	$⊢ A^{(0 ..^S)} \in V$
26	25	rabex	$⊢ \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \in V$
27	26	a1i	$⊢ φ \to \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} \in V$
28	16 21 24 2 27	ovmpod	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$

Metamath Proof Explorer

Theorem reprval

Proof