eldioph2

Description: Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 . (Contributed by Stefan O'Rear, 8-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		mzpcompact2	$⊢ P \in mzPoly (S) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})))$
2	1	3ad2ant3	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \to \exists a \in Fin \exists b \in mzPoly (a) (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})))$
3		fveq1	$⊢ P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) \to P (u) = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u)$
4	3	eqeq1d	$⊢ P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) \to (P (u) = 0 \leftrightarrow (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)$
5	4	anbi2d	$⊢ P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) \to ((t = {u ↾}_{(1 \dots N)} \land P (u) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0))$
6	5	rexbidv	$⊢ P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) \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 ↾}_{a})) (u) = 0))$
7	6	abbidv	$⊢ P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) \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 ↾}_{a})) (u) = 0)\}$
8	7	ad2antll	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \land (a \in Fin \land b \in mzPoly (a))) \land (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})))) \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 ↾}_{a})) (u) = 0)\}$
9		simplll	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to N \in ℕ_{0}$
10		simplrl	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to a \in Fin$
11		fzfi	$⊢ (1 \dots N) \in Fin$
12		unfi	$⊢ (a \in Fin \land (1 \dots N) \in Fin) \to a \cup (1 \dots N) \in Fin$
13	10 11 12	sylancl	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to a \cup (1 \dots N) \in Fin$
14		ssun2	$⊢ (1 \dots N) \subseteq a \cup (1 \dots N)$
15	14	a1i	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to (1 \dots N) \subseteq a \cup (1 \dots N)$
16		eldioph2lem1	$⊢ (N \in ℕ_{0} \land a \cup (1 \dots N) \in Fin \land (1 \dots N) \subseteq a \cup (1 \dots N)) \to \exists c \in ℤ_{\geq N} \exists d \in V (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
17	9 13 15 16	syl3anc	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to \exists c \in ℤ_{\geq N} \exists d \in V (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
18		f1ococnv2	$⊢ d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \to d \circ d^{-1} = {I ↾}_{(a \cup (1 \dots N))}$
19	18	ad2antrl	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to d \circ d^{-1} = {I ↾}_{(a \cup (1 \dots N))}$
20	19	reseq1d	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to {(d \circ d^{-1}) ↾}_{a} = {({I ↾}_{(a \cup (1 \dots N))}) ↾}_{a}$
21		ssun1	$⊢ a \subseteq a \cup (1 \dots N)$
22		resabs1	$⊢ a \subseteq a \cup (1 \dots N) \to {({I ↾}_{(a \cup (1 \dots N))}) ↾}_{a} = {I ↾}_{a}$
23	21 22	ax-mp	$⊢ {({I ↾}_{(a \cup (1 \dots N))}) ↾}_{a} = {I ↾}_{a}$
24	20 23	eqtr2di	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to {I ↾}_{a} = {(d \circ d^{-1}) ↾}_{a}$
25		resco	$⊢ {(d \circ d^{-1}) ↾}_{a} = d \circ ({d^{-1} ↾}_{a})$
26	24 25	eqtrdi	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to {I ↾}_{a} = d \circ ({d^{-1} ↾}_{a})$
27	26	adantr	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to {I ↾}_{a} = d \circ ({d^{-1} ↾}_{a})$
28	27	coeq2d	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to e \circ ({I ↾}_{a}) = e \circ (d \circ ({d^{-1} ↾}_{a}))$
29		coires1	$⊢ e \circ ({I ↾}_{a}) = {e ↾}_{a}$
30		coass	$⊢ (e \circ d) \circ ({d^{-1} ↾}_{a}) = e \circ (d \circ ({d^{-1} ↾}_{a}))$
31	30	eqcomi	$⊢ e \circ (d \circ ({d^{-1} ↾}_{a})) = (e \circ d) \circ ({d^{-1} ↾}_{a})$
32	28 29 31	3eqtr3g	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to {e ↾}_{a} = (e \circ d) \circ ({d^{-1} ↾}_{a})$
33	32	fveq2d	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to b ({e ↾}_{a}) = b ((e \circ d) \circ ({d^{-1} ↾}_{a}))$
34		ovexd	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to (1 \dots c) \in V$
35		simpr	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to e \in (ℤ^{S})$
36		f1of1	$⊢ d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \to d : (1 \dots c) \underset{1-1}{⟶} a \cup (1 \dots N)$
37	36	ad2antrl	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to d : (1 \dots c) \underset{1-1}{⟶} a \cup (1 \dots N)$
38		simpr	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to a \subseteq S$
39		simprr	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \to (1 \dots N) \subseteq S$
40	39	ad2antrr	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to (1 \dots N) \subseteq S$
41	38 40	unssd	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to a \cup (1 \dots N) \subseteq S$
42	41	ad2antrr	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to a \cup (1 \dots N) \subseteq S$
43		f1ss	$⊢ (d : (1 \dots c) \underset{1-1}{⟶} a \cup (1 \dots N) \land a \cup (1 \dots N) \subseteq S) \to d : (1 \dots c) \underset{1-1}{⟶} S$
44	37 42 43	syl2anc	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to d : (1 \dots c) \underset{1-1}{⟶} S$
45		f1f	$⊢ d : (1 \dots c) \underset{1-1}{⟶} S \to d : (1 \dots c) ⟶ S$
46	44 45	syl	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to d : (1 \dots c) ⟶ S$
47	46	adantr	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to d : (1 \dots c) ⟶ S$
48		mapco2g	$⊢ ((1 \dots c) \in V \land e \in (ℤ^{S}) \land d : (1 \dots c) ⟶ S) \to e \circ d \in (ℤ^{(1 \dots c)})$
49	34 35 47 48	syl3anc	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to e \circ d \in (ℤ^{(1 \dots c)})$
50		coeq1	$⊢ h = e \circ d \to h \circ ({d^{-1} ↾}_{a}) = (e \circ d) \circ ({d^{-1} ↾}_{a})$
51	50	fveq2d	$⊢ h = e \circ d \to b (h \circ ({d^{-1} ↾}_{a})) = b ((e \circ d) \circ ({d^{-1} ↾}_{a}))$
52		eqid	$⊢ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) = (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a})))$
53		fvex	$⊢ b ((e \circ d) \circ ({d^{-1} ↾}_{a})) \in V$
54	51 52 53	fvmpt	$⊢ e \circ d \in (ℤ^{(1 \dots c)}) \to (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d) = b ((e \circ d) \circ ({d^{-1} ↾}_{a}))$
55	49 54	syl	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d) = b ((e \circ d) \circ ({d^{-1} ↾}_{a}))$
56	33 55	eqtr4d	$⊢ ((((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \land e \in (ℤ^{S})) \to b ({e ↾}_{a}) = (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)$
57	56	mpteq2dva	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) = (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d))$
58	57	fveq1d	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u)$
59	58	eqeq1d	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to ((e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0 \leftrightarrow (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0)$
60	59	anbi2d	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to ((t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0) \leftrightarrow (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0))$
61	60	rexbidv	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (\exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0) \leftrightarrow \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0))$
62	61	abbidv	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(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 ↾}_{a})) (u) = 0)\} = \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0)\}$
63		simplrl	$⊢ ((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \to S \in V$
64	63	ad3antrrr	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to S \in V$
65		simprr	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
66		diophrw	$⊢ (S \in V \land d : (1 \dots c) \underset{1-1}{⟶} S \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0)\} = \{t \| \exists g \in ({ℕ_{0}}^{(1 \dots c)}) (t = {g ↾}_{(1 \dots N)} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (g) = 0)\}$
67	64 44 65 66	syl3anc	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (e \circ d)) (u) = 0)\} = \{t \| \exists g \in ({ℕ_{0}}^{(1 \dots c)}) (t = {g ↾}_{(1 \dots N)} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (g) = 0)\}$
68	62 67	eqtrd	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(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 ↾}_{a})) (u) = 0)\} = \{t \| \exists g \in ({ℕ_{0}}^{(1 \dots c)}) (t = {g ↾}_{(1 \dots N)} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (g) = 0)\}$
69		simp-5l	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to N \in ℕ_{0}$
70		simplrl	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to c \in ℤ_{\geq N}$
71		ovexd	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (1 \dots c) \in V$
72		simplrr	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to b \in mzPoly (a)$
73	72	ad2antrr	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to b \in mzPoly (a)$
74		f1ocnv	$⊢ d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \to d^{-1} : a \cup (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots c)$
75		f1of	$⊢ d^{-1} : a \cup (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots c) \to d^{-1} : a \cup (1 \dots N) ⟶ (1 \dots c)$
76	74 75	syl	$⊢ d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \to d^{-1} : a \cup (1 \dots N) ⟶ (1 \dots c)$
77		fssres	$⊢ (d^{-1} : a \cup (1 \dots N) ⟶ (1 \dots c) \land a \subseteq a \cup (1 \dots N)) \to ({d^{-1} ↾}_{a}) : a ⟶ (1 \dots c)$
78	76 21 77	sylancl	$⊢ d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \to ({d^{-1} ↾}_{a}) : a ⟶ (1 \dots c)$
79	78	ad2antrl	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to ({d^{-1} ↾}_{a}) : a ⟶ (1 \dots c)$
80		mzprename	$⊢ ((1 \dots c) \in V \land b \in mzPoly (a) \land ({d^{-1} ↾}_{a}) : a ⟶ (1 \dots c)) \to (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) \in mzPoly ((1 \dots c))$
81	71 73 79 80	syl3anc	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) \in mzPoly ((1 \dots c))$
82		eldioph	$⊢ (N \in ℕ_{0} \land c \in ℤ_{\geq N} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) \in mzPoly ((1 \dots c))) \to \{t \| \exists g \in ({ℕ_{0}}^{(1 \dots c)}) (t = {g ↾}_{(1 \dots N)} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (g) = 0)\} \in Dioph (N)$
83	69 70 81 82	syl3anc	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})) \to \{t \| \exists g \in ({ℕ_{0}}^{(1 \dots c)}) (t = {g ↾}_{(1 \dots N)} \land (h \in (ℤ^{(1 \dots c)}) ⟼ b (h \circ ({d^{-1} ↾}_{a}))) (g) = 0)\} \in Dioph (N)$
84	68 83	eqeltrd	$⊢ (((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \land (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(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 ↾}_{a})) (u) = 0)\} \in Dioph (N)$
85	84	ex	$⊢ ((((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \land (c \in ℤ_{\geq N} \land d \in V)) \to ((d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(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 ↾}_{a})) (u) = 0)\} \in Dioph (N))$
86	85	rexlimdvva	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to (\exists c \in ℤ_{\geq N} \exists d \in V (d : (1 \dots c) \underset{1-1 onto}{⟶} a \cup (1 \dots N) \land {d ↾}_{(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 ↾}_{a})) (u) = 0)\} \in Dioph (N))$
87	17 86	mpd	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)\} \in Dioph (N)$
88	87	exp31	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S)) \to ((a \in Fin \land b \in mzPoly (a)) \to (a \subseteq S \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)\} \in Dioph (N)))$
89	88	3adant3	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \to ((a \in Fin \land b \in mzPoly (a)) \to (a \subseteq S \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)\} \in Dioph (N)))$
90	89	imp31	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \land (a \in Fin \land b \in mzPoly (a))) \land a \subseteq S) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)\} \in Dioph (N)$
91	90	adantrr	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \land (a \in Fin \land b \in mzPoly (a))) \land (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})))) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})) (u) = 0)\} \in Dioph (N)$
92	8 91	eqeltrd	$⊢ (((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \land (a \in Fin \land b \in mzPoly (a))) \land (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a})))) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N)$
93	92	ex	$⊢ ((N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \land (a \in Fin \land b \in mzPoly (a))) \to ((a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a}))) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N))$
94	93	rexlimdvva	$⊢ (N \in ℕ_{0} \land (S \in V \land (1 \dots N) \subseteq S) \land P \in mzPoly (S)) \to (\exists a \in Fin \exists b \in mzPoly (a) (a \subseteq S \land P = (e \in (ℤ^{S}) ⟼ b ({e ↾}_{a}))) \to \{t \| \exists u \in ({ℕ_{0}}^{S}) (t = {u ↾}_{(1 \dots N)} \land P (u) = 0)\} \in Dioph (N))$
95	2 94	mpd	$⊢ (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)$

Metamath Proof Explorer

Theorem eldioph2

Proof