eldioph2b

Description: While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ) . For instance, in diophin we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014)

		Ref	Expression
	Assertion	eldioph2b	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to (A \in Dioph (N) \leftrightarrow \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$

Proof

Step	Hyp	Ref	Expression
1		eldiophb	$⊢ A \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists a \in ℤ_{\geq N} \exists b \in mzPoly ((1 \dots a)) A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\})$
2		simp-5r	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to S \in V$
3		simprr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to b \in mzPoly ((1 \dots a))$
4	3	ad2antrr	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to b \in mzPoly ((1 \dots a))$
5		simprl	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to c : (1 \dots a) \underset{1-1}{⟶} S$
6		f1f	$⊢ c : (1 \dots a) \underset{1-1}{⟶} S \to c : (1 \dots a) ⟶ S$
7	5 6	syl	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to c : (1 \dots a) ⟶ S$
8		mzprename	$⊢ (S \in V \land b \in mzPoly ((1 \dots a)) \land c : (1 \dots a) ⟶ S) \to (e \in (ℤ^{S}) ⟼ b (e \circ c)) \in mzPoly (S)$
9	2 4 7 8	syl3anc	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (e \in (ℤ^{S}) ⟼ b (e \circ c)) \in mzPoly (S)$
10		simprr	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
11		diophrw	$⊢ (S \in V \land c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)\} = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\}$
12	11	eqcomd	$⊢ (S \in V \land c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \to \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)\}$
13	2 5 10 12	syl3anc	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)\}$
14		fveq1	$⊢ p = (e \in (ℤ^{S}) ⟼ b (e \circ c)) \to p (u) = (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u)$
15	14	eqeq1d	$⊢ p = (e \in (ℤ^{S}) ⟼ b (e \circ c)) \to (p (u) = 0 \leftrightarrow (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)$
16	15	anbi2d	$⊢ p = (e \in (ℤ^{S}) ⟼ b (e \circ c)) \to ((t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0))$
17	16	rexbidv	$⊢ p = (e \in (ℤ^{S}) ⟼ b (e \circ c)) \to (\exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0))$
18	17	abbidv	$⊢ p = (e \in (ℤ^{S}) ⟼ b (e \circ c)) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)\}$
19	18	rspceeqv	$⊢ ((e \in (ℤ^{S}) ⟼ b (e \circ c)) \in mzPoly (S) \land \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b (e \circ c)) (u) = 0)\}) \to \exists p \in mzPoly (S) \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
20	9 13 19	syl2anc	$⊢ (((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \land c \in V) \land (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to \exists p \in mzPoly (S) \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
21		simplll	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to N \in ℕ_{0}$
22		simplrl	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to \neg S \in Fin$
23		simplrr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to (1 \dots N) \subseteq S$
24		simprl	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to a \in ℤ_{\geq N}$
25		eldioph2lem2	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land a \in ℤ_{\geq N})) \to \exists c (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
26	21 22 23 24 25	syl22anc	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to \exists c (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
27		rexv	$⊢ \exists c \in V (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \leftrightarrow \exists c (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
28	26 27	sylibr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to \exists c \in V (c : (1 \dots a) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
29	20 28	r19.29a	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to \exists p \in mzPoly (S) \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
30		eqeq1	$⊢ A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} \to (A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
31	30	rexbidv	$⊢ A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} \to (\exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow \exists p \in mzPoly (S) \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
32	29 31	syl5ibrcom	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land (a \in ℤ_{\geq N} \land b \in mzPoly ((1 \dots a)))) \to (A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} \to \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
33	32	rexlimdvva	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to (\exists a \in ℤ_{\geq N} \exists b \in mzPoly ((1 \dots a)) A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\} \to \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
34	33	adantld	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to ((N \in ℕ_{0} \land \exists a \in ℤ_{\geq N} \exists b \in mzPoly ((1 \dots a)) A = \{t \| \exists d \in ({ℕ_{0}}^{(1 \dots a)}) (t = {d ↾}_{(1 \dots N)} \land b (d) = 0)\}) \to \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
35	1 34	biimtrid	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to (A \in Dioph (N) \to \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
36		simpr	$⊢ ((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \land A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \to A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}$
37		simplll	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \to N \in ℕ_{0}$
38		simpllr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \to S \in V$
39		simplrr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \to (1 \dots N) \subseteq S$
40		simpr	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \to p \in mzPoly (S)$
41		eldioph2	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land p \in mzPoly (S)) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in Dioph (N)$
42	37 38 39 40 41	syl121anc	$⊢ (((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in Dioph (N)$
43	42	adantr	$⊢ ((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \land A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \in Dioph (N)$
44	36 43	eqeltrd	$⊢ ((((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \land p \in mzPoly (S)) \land A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\}) \to A \in Dioph (N)$
45	44	rexlimdva2	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to (\exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \to A \in Dioph (N))$
46	35 45	impbid	$⊢ ((N \in ℕ_{0} \land S \in V) \land (\neg S \in Fin \land (1 \dots N) \subseteq S)) \to (A \in Dioph (N) \leftrightarrow \exists p \in mzPoly (S) A = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$

Metamath Proof Explorer

Theorem eldioph2b

Proof