eldioph4b

Description: Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (Contributed by Stefan O'Rear, 16-Oct-2014)

	Ref	Expression
Hypotheses	eldioph4b.a	$⊢ W \in V$
	eldioph4b.b	$⊢ \neg W \in Fin$
	eldioph4b.c	$⊢ W \cap ℕ = \emptyset$
Assertion	eldioph4b	$⊢ S \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\})$

Proof

Step	Hyp	Ref	Expression
1		eldioph4b.a	$⊢ W \in V$
2		eldioph4b.b	$⊢ \neg W \in Fin$
3		eldioph4b.c	$⊢ W \cap ℕ = \emptyset$
4		eldiophelnn0	$⊢ S \in Dioph (N) \to N \in ℕ_{0}$
5		ovex	$⊢ (1 \dots N) \in V$
6	1 5	unex	$⊢ W \cup (1 \dots N) \in V$
7	6	jctr	$⊢ N \in ℕ_{0} \to (N \in ℕ_{0} \land W \cup (1 \dots N) \in V)$
8	2	intnanr	$⊢ \neg (W \in Fin \land (1 \dots N) \in Fin)$
9		unfir	$⊢ W \cup (1 \dots N) \in Fin \to (W \in Fin \land (1 \dots N) \in Fin)$
10	8 9	mto	$⊢ \neg W \cup (1 \dots N) \in Fin$
11		ssun2	$⊢ (1 \dots N) \subseteq W \cup (1 \dots N)$
12	10 11	pm3.2i	$⊢ (\neg W \cup (1 \dots N) \in Fin \land (1 \dots N) \subseteq W \cup (1 \dots N))$
13		eldioph2b	$⊢ ((N \in ℕ_{0} \land W \cup (1 \dots N) \in V) \land (\neg W \cup (1 \dots N) \in Fin \land (1 \dots N) \subseteq W \cup (1 \dots N))) \to (S \in Dioph (N) \leftrightarrow \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
14	7 12 13	sylancl	$⊢ N \in ℕ_{0} \to (S \in Dioph (N) \leftrightarrow \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\})$
15		elmapssres	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land (1 \dots N) \subseteq W \cup (1 \dots N)) \to {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
16	11 15	mpan2	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
17	16	adantr	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)})$
18		ssun1	$⊢ W \subseteq W \cup (1 \dots N)$
19		elmapssres	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land W \subseteq W \cup (1 \dots N)) \to {u ↾}_{W} \in ({ℕ_{0}}^{W})$
20	18 19	mpan2	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to {u ↾}_{W} \in ({ℕ_{0}}^{W})$
21	20	adantr	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to {u ↾}_{W} \in ({ℕ_{0}}^{W})$
22		uncom	$⊢ ({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W}) = ({u ↾}_{W}) \cup ({u ↾}_{(1 \dots N)})$
23		resundi	$⊢ {u ↾}_{(W \cup (1 \dots N))} = ({u ↾}_{W}) \cup ({u ↾}_{(1 \dots N)})$
24	22 23	eqtr4i	$⊢ ({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W}) = {u ↾}_{(W \cup (1 \dots N))}$
25		elmapi	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to u : W \cup (1 \dots N) ⟶ ℕ_{0}$
26		ffn	$⊢ u : W \cup (1 \dots N) ⟶ ℕ_{0} \to u Fn (W \cup (1 \dots N))$
27		fnresdm	$⊢ u Fn (W \cup (1 \dots N)) \to {u ↾}_{(W \cup (1 \dots N))} = u$
28	25 26 27	3syl	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to {u ↾}_{(W \cup (1 \dots N))} = u$
29	24 28	eqtrid	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to ({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W}) = u$
30	29	fveqeq2d	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to (p (({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W})) = 0 \leftrightarrow p (u) = 0)$
31	30	biimpar	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to p (({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W})) = 0$
32		uneq2	$⊢ w = {u ↾}_{W} \to ({u ↾}_{(1 \dots N)}) \cup w = ({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W})$
33	32	fveqeq2d	$⊢ w = {u ↾}_{W} \to (p (({u ↾}_{(1 \dots N)}) \cup w) = 0 \leftrightarrow p (({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W})) = 0)$
34	33	rspcev	$⊢ ({u ↾}_{W} \in ({ℕ_{0}}^{W}) \land p (({u ↾}_{(1 \dots N)}) \cup ({u ↾}_{W})) = 0) \to \exists w \in ({ℕ_{0}}^{W}) p (({u ↾}_{(1 \dots N)}) \cup w) = 0$
35	21 31 34	syl2anc	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to \exists w \in ({ℕ_{0}}^{W}) p (({u ↾}_{(1 \dots N)}) \cup w) = 0$
36	17 35	jca	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to ({u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (({u ↾}_{(1 \dots N)}) \cup w) = 0)$
37		eleq1	$⊢ t = {u ↾}_{(1 \dots N)} \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \leftrightarrow {u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}))$
38		uneq1	$⊢ t = {u ↾}_{(1 \dots N)} \to t \cup w = ({u ↾}_{(1 \dots N)}) \cup w$
39	38	fveqeq2d	$⊢ t = {u ↾}_{(1 \dots N)} \to (p (t \cup w) = 0 \leftrightarrow p (({u ↾}_{(1 \dots N)}) \cup w) = 0)$
40	39	rexbidv	$⊢ t = {u ↾}_{(1 \dots N)} \to (\exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0 \leftrightarrow \exists w \in ({ℕ_{0}}^{W}) p (({u ↾}_{(1 \dots N)}) \cup w) = 0)$
41	37 40	anbi12d	$⊢ t = {u ↾}_{(1 \dots N)} \to ((t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0) \leftrightarrow ({u ↾}_{(1 \dots N)} \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (({u ↾}_{(1 \dots N)}) \cup w) = 0))$
42	36 41	syl5ibrcom	$⊢ (u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land p (u) = 0) \to (t = {u ↾}_{(1 \dots N)} \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0))$
43	42	expimpd	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to ((p (u) = 0 \land t = {u ↾}_{(1 \dots N)}) \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0))$
44	43	ancomsd	$⊢ u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \to ((t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0))$
45	44	rexlimiv	$⊢ \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \to (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0)$
46		uncom	$⊢ t \cup w = w \cup t$
47		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
48		sslin	$⊢ (1 \dots N) \subseteq ℕ \to W \cap (1 \dots N) \subseteq W \cap ℕ$
49	47 48	ax-mp	$⊢ W \cap (1 \dots N) \subseteq W \cap ℕ$
50	49 3	sseqtri	$⊢ W \cap (1 \dots N) \subseteq \emptyset$
51		ss0	$⊢ W \cap (1 \dots N) \subseteq \emptyset \to W \cap (1 \dots N) = \emptyset$
52	50 51	ax-mp	$⊢ W \cap (1 \dots N) = \emptyset$
53	52	reseq2i	$⊢ {w ↾}_{(W \cap (1 \dots N))} = {w ↾}_{\emptyset}$
54		res0	$⊢ {w ↾}_{\emptyset} = \emptyset$
55	53 54	eqtri	$⊢ {w ↾}_{(W \cap (1 \dots N))} = \emptyset$
56	52	reseq2i	$⊢ {t ↾}_{(W \cap (1 \dots N))} = {t ↾}_{\emptyset}$
57		res0	$⊢ {t ↾}_{\emptyset} = \emptyset$
58	56 57	eqtri	$⊢ {t ↾}_{(W \cap (1 \dots N))} = \emptyset$
59	55 58	eqtr4i	$⊢ {w ↾}_{(W \cap (1 \dots N))} = {t ↾}_{(W \cap (1 \dots N))}$
60		elmapresaun	$⊢ (w \in ({ℕ_{0}}^{W}) \land t \in ({ℕ_{0}}^{(1 \dots N)}) \land {w ↾}_{(W \cap (1 \dots N))} = {t ↾}_{(W \cap (1 \dots N))}) \to w \cup t \in ({ℕ_{0}}^{(W \cup (1 \dots N))})$
61	59 60	mp3an3	$⊢ (w \in ({ℕ_{0}}^{W}) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to w \cup t \in ({ℕ_{0}}^{(W \cup (1 \dots N))})$
62	61	ancoms	$⊢ (t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \to w \cup t \in ({ℕ_{0}}^{(W \cup (1 \dots N))})$
63	46 62	eqeltrid	$⊢ (t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \to t \cup w \in ({ℕ_{0}}^{(W \cup (1 \dots N))})$
64	63	adantr	$⊢ ((t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \land p (t \cup w) = 0) \to t \cup w \in ({ℕ_{0}}^{(W \cup (1 \dots N))})$
65	46	reseq1i	$⊢ {(t \cup w) ↾}_{(1 \dots N)} = {(w \cup t) ↾}_{(1 \dots N)}$
66		elmapresaunres2	$⊢ (w \in ({ℕ_{0}}^{W}) \land t \in ({ℕ_{0}}^{(1 \dots N)}) \land {w ↾}_{(W \cap (1 \dots N))} = {t ↾}_{(W \cap (1 \dots N))}) \to {(w \cup t) ↾}_{(1 \dots N)} = t$
67	59 66	mp3an3	$⊢ (w \in ({ℕ_{0}}^{W}) \land t \in ({ℕ_{0}}^{(1 \dots N)})) \to {(w \cup t) ↾}_{(1 \dots N)} = t$
68	67	ancoms	$⊢ (t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \to {(w \cup t) ↾}_{(1 \dots N)} = t$
69	65 68	eqtr2id	$⊢ (t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \to t = {(t \cup w) ↾}_{(1 \dots N)}$
70	69	adantr	$⊢ ((t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \land p (t \cup w) = 0) \to t = {(t \cup w) ↾}_{(1 \dots N)}$
71		simpr	$⊢ ((t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \land p (t \cup w) = 0) \to p (t \cup w) = 0$
72		reseq1	$⊢ u = t \cup w \to {u ↾}_{(1 \dots N)} = {(t \cup w) ↾}_{(1 \dots N)}$
73	72	eqeq2d	$⊢ u = t \cup w \to (t = {u ↾}_{(1 \dots N)} \leftrightarrow t = {(t \cup w) ↾}_{(1 \dots N)})$
74		fveqeq2	$⊢ u = t \cup w \to (p (u) = 0 \leftrightarrow p (t \cup w) = 0)$
75	73 74	anbi12d	$⊢ u = t \cup w \to ((t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow (t = {(t \cup w) ↾}_{(1 \dots N)} \land p (t \cup w) = 0))$
76	75	rspcev	$⊢ (t \cup w \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) \land (t = {(t \cup w) ↾}_{(1 \dots N)} \land p (t \cup w) = 0)) \to \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)$
77	64 70 71 76	syl12anc	$⊢ ((t \in ({ℕ_{0}}^{(1 \dots N)}) \land w \in ({ℕ_{0}}^{W})) \land p (t \cup w) = 0) \to \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)$
78	77	r19.29an	$⊢ (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0) \to \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)$
79	45 78	impbii	$⊢ \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0) \leftrightarrow (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0)$
80	79	abbii	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} = \{t \| (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0)\}$
81		df-rab	$⊢ \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\} = \{t \| (t \in ({ℕ_{0}}^{(1 \dots N)}) \land \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0)\}$
82	80 81	eqtr4i	$⊢ \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\}$
83	82	eqeq2i	$⊢ S = \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow S = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\}$
84	83	rexbii	$⊢ \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \| \exists u \in ({ℕ_{0}}^{(W \cup (1 \dots N))}) (t = {u ↾}_{(1 \dots N)} \land p (u) = 0)\} \leftrightarrow \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\}$
85	14 84	bitrdi	$⊢ N \in ℕ_{0} \to (S \in Dioph (N) \leftrightarrow \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\})$
86	4 85	biadanii	$⊢ S \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists p \in mzPoly (W \cup (1 \dots N)) S = \{t \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists w \in ({ℕ_{0}}^{W}) p (t \cup w) = 0\})$

Metamath Proof Explorer

Theorem eldioph4b

Proof