reprdifc

Description: Express the representations as a sum of integers in a difference of sets using conditions on each of the indices. (Contributed by Thierry Arnoux, 27-Dec-2021)

	Ref	Expression
Hypotheses	reprdifc.c	$⊢ C = \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
	reprdifc.a	$⊢ φ \to A \subseteq ℕ$
	reprdifc.b	$⊢ φ \to B \subseteq ℕ$
	reprdifc.m	$⊢ φ \to M \in ℕ_{0}$
	reprdifc.s	$⊢ φ \to S \in ℕ_{0}$
Assertion	reprdifc	$⊢ φ \to (A repr (S) M) ∖ (B repr (S) M) = ⋃_{x \in (0 ..^S)} C$

Proof

Step	Hyp	Ref	Expression
1		reprdifc.c	$⊢ C = \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
2		reprdifc.a	$⊢ φ \to A \subseteq ℕ$
3		reprdifc.b	$⊢ φ \to B \subseteq ℕ$
4		reprdifc.m	$⊢ φ \to M \in ℕ_{0}$
5		reprdifc.s	$⊢ φ \to S \in ℕ_{0}$
6		nfv	$⊢ Ⅎ d φ$
7		nfrab1	$⊢ \underline{Ⅎ} d \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
8		nfcv	$⊢ \underline{Ⅎ} d ⋃_{x \in (0 ..^S)} \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
9	4	nn0zd	$⊢ φ \to M \in ℤ$
10	2 9 5	reprval	$⊢ φ \to A repr (S) M = \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
11	10	eleq2d	$⊢ φ \to (d \in (A repr (S) M) \leftrightarrow d \in \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\})$
12		rabid	$⊢ d \in \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\} \leftrightarrow (d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M)$
13	11 12	bitrdi	$⊢ φ \to (d \in (A repr (S) M) \leftrightarrow (d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M))$
14	13	anbi1d	$⊢ φ \to ((d \in (A repr (S) M) \land \neg d \in (B^{(0 ..^S)})) \leftrightarrow ((d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M) \land \neg d \in (B^{(0 ..^S)})))$
15		eldif	$⊢ d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \leftrightarrow (d \in (A^{(0 ..^S)}) \land \neg d \in (B^{(0 ..^S)}))$
16	15	anbi1i	$⊢ (d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow ((d \in (A^{(0 ..^S)}) \land \neg d \in (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M)$
17		an32	$⊢ ((d \in (A^{(0 ..^S)}) \land \neg d \in (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow ((d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M) \land \neg d \in (B^{(0 ..^S)}))$
18	16 17	bitri	$⊢ (d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow ((d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M) \land \neg d \in (B^{(0 ..^S)}))$
19	18	a1i	$⊢ φ \to ((d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow ((d \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} d (a) = M) \land \neg d \in (B^{(0 ..^S)})))$
20	14 19	bitr4d	$⊢ φ \to ((d \in (A repr (S) M) \land \neg d \in (B^{(0 ..^S)})) \leftrightarrow (d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M))$
21		nnex	$⊢ ℕ \in V$
22	21	a1i	$⊢ φ \to ℕ \in V$
23	22 3	ssexd	$⊢ φ \to B \in V$
24		ovexd	$⊢ φ \to (0 ..^S) \in V$
25		elmapg	$⊢ (B \in V \land (0 ..^S) \in V) \to (d \in (B^{(0 ..^S)}) \leftrightarrow d : (0 ..^S) ⟶ B)$
26	23 24 25	syl2anc	$⊢ φ \to (d \in (B^{(0 ..^S)}) \leftrightarrow d : (0 ..^S) ⟶ B)$
27	26	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to (d \in (B^{(0 ..^S)}) \leftrightarrow d : (0 ..^S) ⟶ B)$
28		ffnfv	$⊢ d : (0 ..^S) ⟶ B \leftrightarrow (d Fn (0 ..^S) \land \forall x \in (0 ..^S) d (x) \in B)$
29	2	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to A \subseteq ℕ$
30	9	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to M \in ℤ$
31	5	adantr	$⊢ (φ \land d \in (A repr (S) M)) \to S \in ℕ_{0}$
32		simpr	$⊢ (φ \land d \in (A repr (S) M)) \to d \in (A repr (S) M)$
33	29 30 31 32	reprf	$⊢ (φ \land d \in (A repr (S) M)) \to d : (0 ..^S) ⟶ A$
34	33	ffnd	$⊢ (φ \land d \in (A repr (S) M)) \to d Fn (0 ..^S)$
35	34	biantrurd	$⊢ (φ \land d \in (A repr (S) M)) \to (\forall x \in (0 ..^S) d (x) \in B \leftrightarrow (d Fn (0 ..^S) \land \forall x \in (0 ..^S) d (x) \in B))$
36	28 35	bitr4id	$⊢ (φ \land d \in (A repr (S) M)) \to (d : (0 ..^S) ⟶ B \leftrightarrow \forall x \in (0 ..^S) d (x) \in B)$
37	27 36	bitrd	$⊢ (φ \land d \in (A repr (S) M)) \to (d \in (B^{(0 ..^S)}) \leftrightarrow \forall x \in (0 ..^S) d (x) \in B)$
38	37	notbid	$⊢ (φ \land d \in (A repr (S) M)) \to (\neg d \in (B^{(0 ..^S)}) \leftrightarrow \neg \forall x \in (0 ..^S) d (x) \in B)$
39		rexnal	$⊢ \exists x \in (0 ..^S) \neg d (x) \in B \leftrightarrow \neg \forall x \in (0 ..^S) d (x) \in B$
40	38 39	bitr4di	$⊢ (φ \land d \in (A repr (S) M)) \to (\neg d \in (B^{(0 ..^S)}) \leftrightarrow \exists x \in (0 ..^S) \neg d (x) \in B)$
41	40	pm5.32da	$⊢ φ \to ((d \in (A repr (S) M) \land \neg d \in (B^{(0 ..^S)})) \leftrightarrow (d \in (A repr (S) M) \land \exists x \in (0 ..^S) \neg d (x) \in B))$
42	20 41	bitr3d	$⊢ φ \to ((d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow (d \in (A repr (S) M) \land \exists x \in (0 ..^S) \neg d (x) \in B))$
43		fveq1	$⊢ c = d \to c (x) = d (x)$
44	43	eleq1d	$⊢ c = d \to (c (x) \in B \leftrightarrow d (x) \in B)$
45	44	notbid	$⊢ c = d \to (\neg c (x) \in B \leftrightarrow \neg d (x) \in B)$
46	45	elrab	$⊢ d \in \{c \in (A repr (S) M) \| \neg c (x) \in B\} \leftrightarrow (d \in (A repr (S) M) \land \neg d (x) \in B)$
47	46	rexbii	$⊢ \exists x \in (0 ..^S) d \in \{c \in (A repr (S) M) \| \neg c (x) \in B\} \leftrightarrow \exists x \in (0 ..^S) (d \in (A repr (S) M) \land \neg d (x) \in B)$
48		r19.42v	$⊢ \exists x \in (0 ..^S) (d \in (A repr (S) M) \land \neg d (x) \in B) \leftrightarrow (d \in (A repr (S) M) \land \exists x \in (0 ..^S) \neg d (x) \in B)$
49	47 48	bitri	$⊢ \exists x \in (0 ..^S) d \in \{c \in (A repr (S) M) \| \neg c (x) \in B\} \leftrightarrow (d \in (A repr (S) M) \land \exists x \in (0 ..^S) \neg d (x) \in B)$
50	42 49	bitr4di	$⊢ φ \to ((d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M) \leftrightarrow \exists x \in (0 ..^S) d \in \{c \in (A repr (S) M) \| \neg c (x) \in B\})$
51		rabid	$⊢ d \in \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\} \leftrightarrow (d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} d (a) = M)$
52		eliun	$⊢ d \in ⋃_{x \in (0 ..^S)} \{c \in (A repr (S) M) \| \neg c (x) \in B\} \leftrightarrow \exists x \in (0 ..^S) d \in \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
53	50 51 52	3bitr4g	$⊢ φ \to (d \in \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\} \leftrightarrow d \in ⋃_{x \in (0 ..^S)} \{c \in (A repr (S) M) \| \neg c (x) \in B\})$
54	6 7 8 53	eqrd	$⊢ φ \to \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\} = ⋃_{x \in (0 ..^S)} \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
55	3 9 5	reprval	$⊢ φ \to B repr (S) M = \{d \in (B^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
56	10 55	difeq12d	$⊢ φ \to (A repr (S) M) ∖ (B repr (S) M) = \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\} ∖ \{d \in (B^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
57		difrab2	$⊢ \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\} ∖ \{d \in (B^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M\} = \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
58	56 57	eqtrdi	$⊢ φ \to (A repr (S) M) ∖ (B repr (S) M) = \{d \in ((A^{(0 ..^S)}) ∖ (B^{(0 ..^S)})) \| \sum_{a \in (0 ..^S)} d (a) = M\}$
59	1	a1i	$⊢ φ \to C = \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
60	59	iuneq2d	$⊢ φ \to ⋃_{x \in (0 ..^S)} C = ⋃_{x \in (0 ..^S)} \{c \in (A repr (S) M) \| \neg c (x) \in B\}$
61	54 58 60	3eqtr4d	$⊢ φ \to (A repr (S) M) ∖ (B repr (S) M) = ⋃_{x \in (0 ..^S)} C$

Metamath Proof Explorer

Theorem reprdifc

Proof