eldioph3

Description: Inference version of eldioph3b with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ_{0} \land P \in mzPoly (ℕ)) \to N \in ℕ_{0}$
2		simpr	$⊢ (N \in ℕ_{0} \land P \in mzPoly (ℕ)) \to P \in mzPoly (ℕ)$
3		eqidd	$⊢ (N \in ℕ_{0} \land P \in mzPoly (ℕ)) \to \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}$
4		fveq1	$⊢ p = P \to p (b) = P (b)$
5	4	eqeq1d	$⊢ p = P \to (p (b) = 0 \leftrightarrow P (b) = 0)$
6	5	anbi2d	$⊢ p = P \to ((a = {b ↾}_{(1 \dots N)} \land p (b) = 0) \leftrightarrow (a = {b ↾}_{(1 \dots N)} \land P (b) = 0))$
7	6	rexbidv	$⊢ p = P \to (\exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0) \leftrightarrow \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land P (b) = 0))$
8	7	abbidv	$⊢ p = P \to \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0)\} = \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land P (b) = 0)\}$
9		eqeq1	$⊢ a = t \to (a = {b ↾}_{(1 \dots N)} \leftrightarrow t = {b ↾}_{(1 \dots N)})$
10	9	anbi1d	$⊢ a = t \to ((a = {b ↾}_{(1 \dots N)} \land P (b) = 0) \leftrightarrow (t = {b ↾}_{(1 \dots N)} \land P (b) = 0))$
11	10	rexbidv	$⊢ a = t \to (\exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land P (b) = 0) \leftrightarrow \exists b \in ({ℕ_{0}}^{ℕ}) (t = {b ↾}_{(1 \dots N)} \land P (b) = 0))$
12		reseq1	$⊢ b = u \to {b ↾}_{(1 \dots N)} = {u ↾}_{(1 \dots N)}$
13	12	eqeq2d	$⊢ b = u \to (t = {b ↾}_{(1 \dots N)} \leftrightarrow t = {u ↾}_{(1 \dots N)})$
14		fveqeq2	$⊢ b = u \to (P (b) = 0 \leftrightarrow P (u) = 0)$
15	13 14	anbi12d	$⊢ b = u \to ((t = {b ↾}_{(1 \dots N)} \land P (b) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land P (u) = 0))$
16	15	cbvrexvw	$⊢ \exists b \in ({ℕ_{0}}^{ℕ}) (t = {b ↾}_{(1 \dots N)} \land P (b) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)$
17	11 16	bitrdi	$⊢ a = t \to (\exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land P (b) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0))$
18	17	cbvabv	$⊢ \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land P (b) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}$
19	8 18	eqtrdi	$⊢ p = P \to \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}$
20	19	rspceeqv	$⊢ (P \in mzPoly (ℕ) \land \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\}) \to \exists p \in mzPoly (ℕ) \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0)\}$
21	2 3 20	syl2anc	$⊢ (N \in ℕ_{0} \land P \in mzPoly (ℕ)) \to \exists p \in mzPoly (ℕ) \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0)\}$
22		eldioph3b	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists p \in mzPoly (ℕ) \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} = \{a \| \exists b \in ({ℕ_{0}}^{ℕ}) (a = {b ↾}_{(1 \dots N)} \land p (b) = 0)\})$
23	1 21 22	sylanbrc	$⊢ (N \in ℕ_{0} \land P \in mzPoly (ℕ)) \to \{t \| \exists u \in ({ℕ_{0}}^{ℕ}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N)$

Metamath Proof Explorer

Theorem eldioph3

Proof