diophrex

Description: Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	diophrex	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \to \{t \| \exists u \in S t = {u ↾}_{(1 \dots N)}\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ a = t \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow t = {b ↾}_{(1 \dots N)})$
2	1	rexbidv	$⊢ a = t \to (\exists b \in S a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists b \in S t = {b ↾}_{(1 \dots N)})$
3		reseq1	$⊢ b = u \to {b ↾}_{(1 \dots N)} = {u ↾}_{(1 \dots N)}$
4	3	eqeq2d	$⊢ b = u \to (t = {b ↾}_{(1 \dots N)} \leftrightarrow t = {u ↾}_{(1 \dots N)})$
5	4	cbvrexvw	$⊢ \exists b \in S t = {b ↾}_{(1 \dots N)} \leftrightarrow \exists u \in S t = {u ↾}_{(1 \dots N)}$
6	2 5	syl6bb	$⊢ a = t \to (\exists b \in S a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists u \in S t = {u ↾}_{(1 \dots N)})$
7	6	cbvabv	$⊢ \{a \| \exists b \in S a = {b ↾}_{(1 \dots N)}\} = \{t \| \exists u \in S t = {u ↾}_{(1 \dots N)}\}$
8		rexeq	$⊢ S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} \to (\exists b \in S a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)})$
9	8	abbidv	$⊢ S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} \to \{a \| \exists b \in S a = {b ↾}_{(1 \dots N)}\} = \{a \| \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)}\}$
10	9	adantl	$⊢ (((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \land S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\}) \to \{a \| \exists b \in S a = {b ↾}_{(1 \dots N)}\} = \{a \| \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)}\}$
11		eqeq1	$⊢ d = b \to (d = {e ↾}_{(1 \dots M)} \leftrightarrow b = {e ↾}_{(1 \dots M)})$
12	11	anbi1d	$⊢ d = b \to ((d = {e ↾}_{(1 \dots M)} \land c (e) = 0) \leftrightarrow (b = {e ↾}_{(1 \dots M)} \land c (e) = 0))$
13	12	rexbidv	$⊢ d = b \to (\exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0) \leftrightarrow \exists e \in ({ℕ_{0}}^{ℕ}) (b = {e ↾}_{(1 \dots M)} \land c (e) = 0))$
14	13	rexab	$⊢ \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists b (\exists e \in ({ℕ_{0}}^{ℕ}) (b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)})$
15		r19.41v	$⊢ \exists e \in ({ℕ_{0}}^{ℕ}) ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (\exists e \in ({ℕ_{0}}^{ℕ}) (b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)})$
16	15	exbii	$⊢ \exists b \exists e \in ({ℕ_{0}}^{ℕ}) ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists b (\exists e \in ({ℕ_{0}}^{ℕ}) (b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)})$
17		rexcom4	$⊢ \exists e \in ({ℕ_{0}}^{ℕ}) \exists b ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists b \exists e \in ({ℕ_{0}}^{ℕ}) ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)})$
18		anass	$⊢ ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (b = {e ↾}_{(1 \dots M)} \land (c (e) = 0 \land a = {b ↾}_{(1 \dots N)}))$
19	18	exbii	$⊢ \exists b ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists b (b = {e ↾}_{(1 \dots M)} \land (c (e) = 0 \land a = {b ↾}_{(1 \dots N)}))$
20		vex	$⊢ e \in V$
21	20	resex	$⊢ {e ↾}_{(1 \dots M)} \in V$
22		reseq1	$⊢ b = {e ↾}_{(1 \dots M)} \to {b ↾}_{(1 \dots N)} = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)}$
23	22	eqeq2d	$⊢ b = {e ↾}_{(1 \dots M)} \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)})$
24	23	anbi2d	$⊢ b = {e ↾}_{(1 \dots M)} \to ((c (e) = 0 \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (c (e) = 0 \land a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)}))$
25	21 24	ceqsexv	$⊢ \exists b (b = {e ↾}_{(1 \dots M)} \land (c (e) = 0 \land a = {b ↾}_{(1 \dots N)})) \leftrightarrow (c (e) = 0 \land a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)})$
26	19 25	bitri	$⊢ \exists b ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (c (e) = 0 \land a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)})$
27		ancom	$⊢ (c (e) = 0 \land a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)}) \leftrightarrow (a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)} \land c (e) = 0)$
28		simpl2	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to M \in ℤ_{\geq N}$
29		fzss2	$⊢ M \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots M)$
30		resabs1	$⊢ (1 \dots N) \subseteq (1 \dots M) \to {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)} = {e ↾}_{(1 \dots N)}$
31	28 29 30	3syl	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)} = {e ↾}_{(1 \dots N)}$
32	31	eqeq2d	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)} \leftrightarrow a = {e ↾}_{(1 \dots N)})$
33	32	anbi1d	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to ((a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)} \land c (e) = 0) \leftrightarrow (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
34	27 33	syl5bb	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to ((c (e) = 0 \land a = {({e ↾}_{(1 \dots M)}) ↾}_{(1 \dots N)}) \leftrightarrow (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
35	26 34	syl5bb	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (\exists b ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
36	35	rexbidv	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (\exists e \in ({ℕ_{0}}^{ℕ}) \exists b ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
37	17 36	bitr3id	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (\exists b \exists e \in ({ℕ_{0}}^{ℕ}) ((b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
38	16 37	bitr3id	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (\exists b (\exists e \in ({ℕ_{0}}^{ℕ}) (b = {e ↾}_{(1 \dots M)} \land c (e) = 0) \land a = {b ↾}_{(1 \dots N)}) \leftrightarrow \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
39	14 38	syl5bb	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to (\exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)} \leftrightarrow \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0))$
40	39	abbidv	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to \{a \| \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)}\} = \{a \| \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0)\}$
41		eldioph3	$⊢ (N \in ℕ_{0} \land c \in mzPoly (ℕ)) \to \{a \| \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0)\} \in Dioph (N)$
42	41	3ad2antl1	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to \{a \| \exists e \in ({ℕ_{0}}^{ℕ}) (a = {e ↾}_{(1 \dots N)} \land c (e) = 0)\} \in Dioph (N)$
43	40 42	eqeltrd	$⊢ ((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \to \{a \| \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
44	43	adantr	$⊢ (((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \land S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\}) \to \{a \| \exists b \in \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\} a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
45	10 44	eqeltrd	$⊢ (((N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \land c \in mzPoly (ℕ)) \land S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\}) \to \{a \| \exists b \in S a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
46		eldioph3b	$⊢ S \in Dioph (M) \leftrightarrow (M \in ℕ_{0} \land \exists c \in mzPoly (ℕ) S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\})$
47	46	simprbi	$⊢ S \in Dioph (M) \to \exists c \in mzPoly (ℕ) S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\}$
48	47	3ad2ant3	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \to \exists c \in mzPoly (ℕ) S = \{d \| \exists e \in ({ℕ_{0}}^{ℕ}) (d = {e ↾}_{(1 \dots M)} \land c (e) = 0)\}$
49	45 48	r19.29a	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \to \{a \| \exists b \in S a = {b ↾}_{(1 \dots N)}\} \in Dioph (N)$
50	7 49	eqeltrrid	$⊢ (N \in ℕ_{0} \land M \in ℤ_{\geq N} \land S \in Dioph (M)) \to \{t \| \exists u \in S t = {u ↾}_{(1 \dots N)}\} \in Dioph (N)$

Metamath Proof Explorer

Theorem diophrex

Proof