eq0rabdioph

Description: This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Assertion	eq0rabdioph	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ t N \in ℕ_{0}$
2		nfmpt1	$⊢ \underline{Ⅎ} t (t \in (ℤ^{(1 \dots N)}) ⟼ A)$
3	2	nfel1	$⊢ Ⅎ t (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))$
4	1 3	nfan	$⊢ Ⅎ t (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)))$
5		zex	$⊢ ℤ \in V$
6		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
7		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
8	5 6 7	mp2an	$⊢ {ℕ_{0}}^{(1 \dots N)} \subseteq ℤ^{(1 \dots N)}$
9	8	sseli	$⊢ t \in ({ℕ_{0}}^{(1 \dots N)}) \to t \in (ℤ^{(1 \dots N)})$
10	9	adantl	$⊢ ((N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to t \in (ℤ^{(1 \dots N)})$
11		mzpf	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
12		mptfcl	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ \to (t \in (ℤ^{(1 \dots N)}) \to A \in ℤ)$
13	12	imp	$⊢ ((t \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ \land t \in (ℤ^{(1 \dots N)})) \to A \in ℤ$
14	11 9 13	syl2an	$⊢ ((t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to A \in ℤ$
15	14	adantll	$⊢ ((N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to A \in ℤ$
16		eqid	$⊢ (t \in (ℤ^{(1 \dots N)}) ⟼ A) = (t \in (ℤ^{(1 \dots N)}) ⟼ A)$
17	16	fvmpt2	$⊢ (t \in (ℤ^{(1 \dots N)}) \land A \in ℤ) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = A$
18	10 15 17	syl2anc	$⊢ ((N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = A$
19	18	eqcomd	$⊢ ((N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to A = (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t)$
20	19	eqeq1d	$⊢ ((N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to (A = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0)$
21	20	ex	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \to (A = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0))$
22	4 21	ralrimi	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0)$
23		rabbi	$⊢ \forall t \in ({ℕ_{0}}^{(1 \dots N)}) (A = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0) \leftrightarrow \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0\}$
24	22 23	sylib	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0\}$
25		nfcv	$⊢ \underline{Ⅎ} t ({ℕ_{0}}^{(1 \dots N)})$
26		nfcv	$⊢ \underline{Ⅎ} a ({ℕ_{0}}^{(1 \dots N)})$
27		nfv	$⊢ Ⅎ a (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0$
28		nffvmpt1	$⊢ \underline{Ⅎ} t (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a)$
29	28	nfeq1	$⊢ Ⅎ t (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0$
30		fveqeq2	$⊢ t = a \to ((t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)$
31	25 26 27 29 30	cbvrabw	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (t) = 0\} = \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0\}$
32	24 31	eqtrdi	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} = \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0\}$
33		df-rab	$⊢ \{a \in ({ℕ_{0}}^{(1 \dots N)}) \| (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0\} = \{a \| (a \in ({ℕ_{0}}^{(1 \dots N)}) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)\}$
34	32 33	eqtrdi	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} = \{a \| (a \in ({ℕ_{0}}^{(1 \dots N)}) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)\}$
35		elmapi	$⊢ b \in ({ℕ_{0}}^{(1 \dots N)}) \to b : (1 \dots N) ⟶ ℕ_{0}$
36		ffn	$⊢ b : (1 \dots N) ⟶ ℕ_{0} \to b Fn (1 \dots N)$
37		fnresdm	$⊢ b Fn (1 \dots N) \to {b ↾}_{(1 \dots N)} = b$
38	35 36 37	3syl	$⊢ b \in ({ℕ_{0}}^{(1 \dots N)}) \to {b ↾}_{(1 \dots N)} = b$
39	38	eqeq2d	$⊢ b \in ({ℕ_{0}}^{(1 \dots N)}) \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow a = b)$
40		equcom	$⊢ a = b \leftrightarrow b = a$
41	39 40	syl6bb	$⊢ b \in ({ℕ_{0}}^{(1 \dots N)}) \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow b = a)$
42	41	anbi1d	$⊢ b \in ({ℕ_{0}}^{(1 \dots N)}) \to ((a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0) \leftrightarrow (b = a \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0))$
43	42	rexbiia	$⊢ \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0) \leftrightarrow \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (b = a \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)$
44		fveqeq2	$⊢ b = a \to ((t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0 \leftrightarrow (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)$
45	44	ceqsrexbv	$⊢ \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (b = a \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0) \leftrightarrow (a \in ({ℕ_{0}}^{(1 \dots N)}) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)$
46	43 45	bitr2i	$⊢ (a \in ({ℕ_{0}}^{(1 \dots N)}) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0) \leftrightarrow \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)$
47	46	abbii	$⊢ \{a \| (a \in ({ℕ_{0}}^{(1 \dots N)}) \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (a) = 0)\} = \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)\}$
48	34 47	eqtrdi	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} = \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)\}$
49		simpl	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to N \in ℕ_{0}$
50		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
51		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
52	50 51	syl	$⊢ N \in ℕ_{0} \to N \in ℤ_{\geq N}$
53	52	adantr	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to N \in ℤ_{\geq N}$
54		simpr	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))$
55		eldioph	$⊢ (N \in ℕ_{0} \land N \in ℤ_{\geq N} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)\} \in Dioph (N)$
56	49 53 54 55	syl3anc	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{a \| \exists b \in ({ℕ_{0}}^{(1 \dots N)}) (a = {b ↾}_{(1 \dots N)} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) (b) = 0)\} \in Dioph (N)$
57	48 56	eqeltrd	$⊢ (N \in ℕ_{0} \land (t \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| A = 0\} \in Dioph (N)$

Metamath Proof Explorer

Theorem eq0rabdioph

Proof