repr0

Description: There is exactly one representation with no elements (an empty sum), only for M = 0 . (Contributed by Thierry Arnoux, 2-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
Assertion	repr0	$⊢ φ \to A repr (0) M = if (M = 0, \{\emptyset\}, \emptyset)$

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		0nn0	$⊢ 0 \in ℕ_{0}$
5	4	a1i	$⊢ φ \to 0 \in ℕ_{0}$
6	1 2 5	reprval	$⊢ φ \to A repr (0) M = \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\}$
7		fzo0	$⊢ (0 ..^0) = \emptyset$
8	7	sumeq1i	$⊢ \sum_{a \in (0 ..^0)} c (a) = \sum_{a \in \emptyset} c (a)$
9		sum0	$⊢ \sum_{a \in \emptyset} c (a) = 0$
10	8 9	eqtri	$⊢ \sum_{a \in (0 ..^0)} c (a) = 0$
11	10	eqeq1i	$⊢ \sum_{a \in (0 ..^0)} c (a) = M \leftrightarrow 0 = M$
12	11	a1i	$⊢ c = \emptyset \to (\sum_{a \in (0 ..^0)} c (a) = M \leftrightarrow 0 = M)$
13		0ex	$⊢ \emptyset \in V$
14	13	snid	$⊢ \emptyset \in \{\emptyset\}$
15		nnex	$⊢ ℕ \in V$
16	15	a1i	$⊢ φ \to ℕ \in V$
17	16 1	ssexd	$⊢ φ \to A \in V$
18		mapdm0	$⊢ A \in V \to A^{\emptyset} = \{\emptyset\}$
19	17 18	syl	$⊢ φ \to A^{\emptyset} = \{\emptyset\}$
20	14 19	eleqtrrid	$⊢ φ \to \emptyset \in (A^{\emptyset})$
21	7	oveq2i	$⊢ A^{(0 ..^0)} = A^{\emptyset}$
22	20 21	eleqtrrdi	$⊢ φ \to \emptyset \in (A^{(0 ..^0)})$
23	22	adantr	$⊢ (φ \land M = 0) \to \emptyset \in (A^{(0 ..^0)})$
24		simpr	$⊢ (φ \land M = 0) \to M = 0$
25	24	eqcomd	$⊢ (φ \land M = 0) \to 0 = M$
26	21 19	eqtrid	$⊢ φ \to A^{(0 ..^0)} = \{\emptyset\}$
27	26	eleq2d	$⊢ φ \to (c \in (A^{(0 ..^0)}) \leftrightarrow c \in \{\emptyset\})$
28	27	biimpa	$⊢ (φ \land c \in (A^{(0 ..^0)})) \to c \in \{\emptyset\}$
29		elsni	$⊢ c \in \{\emptyset\} \to c = \emptyset$
30	28 29	syl	$⊢ (φ \land c \in (A^{(0 ..^0)})) \to c = \emptyset$
31	30	ad4ant13	$⊢ (((φ \land M = 0) \land c \in (A^{(0 ..^0)})) \land \sum_{a \in (0 ..^0)} c (a) = M) \to c = \emptyset$
32	12 23 25 31	rabeqsnd	$⊢ (φ \land M = 0) \to \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\} = \{\emptyset\}$
33	32	eqcomd	$⊢ (φ \land M = 0) \to \{\emptyset\} = \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\}$
34	10	a1i	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to \sum_{a \in (0 ..^0)} c (a) = 0$
35		simplr	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to \neg M = 0$
36	35	neqned	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to M \neq 0$
37	36	necomd	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to 0 \neq M$
38	34 37	eqnetrd	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to \sum_{a \in (0 ..^0)} c (a) \neq M$
39	38	neneqd	$⊢ ((φ \land \neg M = 0) \land c \in (A^{(0 ..^0)})) \to \neg \sum_{a \in (0 ..^0)} c (a) = M$
40	39	ralrimiva	$⊢ (φ \land \neg M = 0) \to \forall c \in (A^{(0 ..^0)}) \neg \sum_{a \in (0 ..^0)} c (a) = M$
41		rabeq0	$⊢ \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\} = \emptyset \leftrightarrow \forall c \in (A^{(0 ..^0)}) \neg \sum_{a \in (0 ..^0)} c (a) = M$
42	40 41	sylibr	$⊢ (φ \land \neg M = 0) \to \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\} = \emptyset$
43	42	eqcomd	$⊢ (φ \land \neg M = 0) \to \emptyset = \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\}$
44	33 43	ifeqda	$⊢ φ \to if (M = 0, \{\emptyset\}, \emptyset) = \{c \in (A^{(0 ..^0)}) \| \sum_{a \in (0 ..^0)} c (a) = M\}$
45	6 44	eqtr4d	$⊢ φ \to A repr (0) M = if (M = 0, \{\emptyset\}, \emptyset)$

Metamath Proof Explorer

Theorem repr0

Proof