eldioph

Description: Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014)

		Ref	Expression
	Assertion	eldioph	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to N \in ℕ_{0}$
2		simp2	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to K \in ℤ_{\geq N}$
3		simp3	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to P \in mzPoly ((1 \dots K))$
4		eqidd	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}$
5		fveq1	$⊢ p = P \to p (u) = P (u)$
6	5	eqeq1d	$⊢ p = P \to (p (u) = 0 \leftrightarrow P (u) = 0)$
7	6	anbi2d	$⊢ p = P \to ((t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land P (u) = 0))$
8	7	rexbidv	$⊢ p = P \to (\exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0))$
9	8	abbidv	$⊢ p = P \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}$
10	9	rspceeqv	$⊢ (P \in mzPoly ((1 \dots K)) \land \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}) \to \exists p \in mzPoly ((1 \dots K)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
11	3 4 10	syl2anc	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to \exists p \in mzPoly ((1 \dots K)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
12		oveq2	$⊢ k = K \to (1 \dots k) = (1 \dots K)$
13	12	fveq2d	$⊢ k = K \to mzPoly ((1 \dots k)) = mzPoly ((1 \dots K))$
14	12	oveq2d	$⊢ k = K \to {ℕ_{0}}^{(1 \dots k)} = {ℕ_{0}}^{(1 \dots K)}$
15	14	rexeqdv	$⊢ k = K \to (\exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0))$
16	15	abbidv	$⊢ k = K \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
17	16	eqeq2d	$⊢ k = K \to (\{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
18	13 17	rexeqbidv	$⊢ k = K \to (\exists p \in mzPoly ((1 \dots k)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow \exists p \in mzPoly ((1 \dots K)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
19	18	rspcev	$⊢ (K \in ℤ_{\geq N} \land \exists p \in mzPoly ((1 \dots K)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \to \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
20	2 11 19	syl2anc	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
21		eldiophb	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists k \in ℤ_{\geq N} \exists p \in mzPoly ((1 \dots k)) \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots k)}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
22	1 20 21	sylanbrc	$⊢ (N \in ℕ_{0} \land K \in ℤ_{\geq N} \land P \in mzPoly ((1 \dots K))) \to \{t \| \exists u \in ({ℕ_{0}}^{(1 \dots K)}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N)$

Metamath Proof Explorer

Theorem eldioph

Proof