diophren

Description: Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014) (Revised by Stefan O'Rear, 5-Jun-2015)

		Ref	Expression
	Assertion	diophren	$⊢ (S \in Dioph (N) \land M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M)$

Proof

Step	Hyp	Ref	Expression
1		zex	$⊢ ℤ \in V$
2		difexg	$⊢ ℤ \in V \to ℤ ∖ ℕ \in V$
3	1 2	ax-mp	$⊢ ℤ ∖ ℕ \in V$
4		ominf	$⊢ \neg ω \in Fin$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6		0p1e1	$⊢ 0 + 1 = 1$
7	6	fveq2i	$⊢ ℤ_{\geq (0 + 1)} = ℤ_{\geq 1}$
8	5 7	eqtr4i	$⊢ ℕ = ℤ_{\geq (0 + 1)}$
9	8	difeq2i	$⊢ ℤ ∖ ℕ = ℤ ∖ ℤ_{\geq (0 + 1)}$
10		0z	$⊢ 0 \in ℤ$
11		lzenom	$⊢ 0 \in ℤ \to (ℤ ∖ ℤ_{\geq (0 + 1)}) \approx ω$
12	10 11	ax-mp	$⊢ (ℤ ∖ ℤ_{\geq (0 + 1)}) \approx ω$
13	9 12	eqbrtri	$⊢ (ℤ ∖ ℕ) \approx ω$
14		enfi	$⊢ (ℤ ∖ ℕ) \approx ω \to (ℤ ∖ ℕ \in Fin \leftrightarrow ω \in Fin)$
15	13 14	ax-mp	$⊢ ℤ ∖ ℕ \in Fin \leftrightarrow ω \in Fin$
16	4 15	mtbir	$⊢ \neg ℤ ∖ ℕ \in Fin$
17		incom	$⊢ (ℤ ∖ ℕ) \cap ℕ = ℕ \cap (ℤ ∖ ℕ)$
18		disjdif	$⊢ ℕ \cap (ℤ ∖ ℕ) = \emptyset$
19	17 18	eqtri	$⊢ (ℤ ∖ ℕ) \cap ℕ = \emptyset$
20	3 16 19	eldioph4b	$⊢ S \in Dioph (N) \leftrightarrow (N \in ℕ_{0} \land \exists b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N)) S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\})$
21		simpr	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to a \in ({ℕ_{0}}^{(1 \dots M)})$
22		simp-4r	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to F : (1 \dots N) ⟶ (1 \dots M)$
23		ovex	$⊢ (1 \dots N) \in V$
24	23	mapco2	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land F : (1 \dots N) ⟶ (1 \dots M)) \to a \circ F \in ({ℕ_{0}}^{(1 \dots N)})$
25	21 22 24	syl2anc	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to a \circ F \in ({ℕ_{0}}^{(1 \dots N)})$
26		uneq1	$⊢ c = a \circ F \to c \cup d = (a \circ F) \cup d$
27	26	fveqeq2d	$⊢ c = a \circ F \to (b (c \cup d) = 0 \leftrightarrow b ((a \circ F) \cup d) = 0)$
28	27	rexbidv	$⊢ c = a \circ F \to (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0 \leftrightarrow \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b ((a \circ F) \cup d) = 0)$
29	28	elrab3	$⊢ a \circ F \in ({ℕ_{0}}^{(1 \dots N)}) \to (a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \leftrightarrow \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b ((a \circ F) \cup d) = 0)$
30	25 29	syl	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to (a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \leftrightarrow \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b ((a \circ F) \cup d) = 0)$
31		simp-5r	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to F : (1 \dots N) ⟶ (1 \dots M)$
32		simplr	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \in ({ℕ_{0}}^{(1 \dots M)})$
33		simpr	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})$
34		coundi	$⊢ (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) = ((a \cup d) \circ F) \cup ((a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}))$
35		coundir	$⊢ (a \cup d) \circ F = (a \circ F) \cup (d \circ F)$
36		elmapi	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to d : ℤ ∖ ℕ ⟶ ℕ_{0}$
37	36	3ad2ant3	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d : ℤ ∖ ℕ ⟶ ℕ_{0}$
38		simp1	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to F : (1 \dots N) ⟶ (1 \dots M)$
39		incom	$⊢ (ℤ ∖ ℕ) \cap (1 \dots M) = (1 \dots M) \cap (ℤ ∖ ℕ)$
40		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
41		ssdisj	$⊢ ((1 \dots M) \subseteq ℕ \land ℕ \cap (ℤ ∖ ℕ) = \emptyset) \to (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset$
42	40 18 41	mp2an	$⊢ (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset$
43	39 42	eqtri	$⊢ (ℤ ∖ ℕ) \cap (1 \dots M) = \emptyset$
44	43	a1i	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (ℤ ∖ ℕ) \cap (1 \dots M) = \emptyset$
45		coeq0i	$⊢ (d : ℤ ∖ ℕ ⟶ ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M) \land (ℤ ∖ ℕ) \cap (1 \dots M) = \emptyset) \to d \circ F = \emptyset$
46	37 38 44 45	syl3anc	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d \circ F = \emptyset$
47	46	uneq2d	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \circ F) \cup (d \circ F) = (a \circ F) \cup \emptyset$
48	35 47	syl5eq	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \cup d) \circ F = (a \circ F) \cup \emptyset$
49		un0	$⊢ (a \circ F) \cup \emptyset = a \circ F$
50	48 49	eqtrdi	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \cup d) \circ F = a \circ F$
51		coundir	$⊢ (a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}) = (a \circ ({I ↾}_{(ℤ ∖ ℕ)})) \cup (d \circ ({I ↾}_{(ℤ ∖ ℕ)}))$
52		elmapi	$⊢ a \in ({ℕ_{0}}^{(1 \dots M)}) \to a : (1 \dots M) ⟶ ℕ_{0}$
53	52	3ad2ant2	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a : (1 \dots M) ⟶ ℕ_{0}$
54		f1oi	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ \underset{1-1 onto}{⟶} ℤ ∖ ℕ$
55		f1of	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ \underset{1-1 onto}{⟶} ℤ ∖ ℕ \to ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
56	54 55	ax-mp	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
57		coeq0i	$⊢ (a : (1 \dots M) ⟶ ℕ_{0} \land ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ \land (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset) \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
58	56 42 57	mp3an23	$⊢ a : (1 \dots M) ⟶ ℕ_{0} \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
59	53 58	syl	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
60		coires1	$⊢ d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = {d ↾}_{(ℤ ∖ ℕ)}$
61		ffn	$⊢ d : ℤ ∖ ℕ ⟶ ℕ_{0} \to d Fn (ℤ ∖ ℕ)$
62		fnresdm	$⊢ d Fn (ℤ ∖ ℕ) \to {d ↾}_{(ℤ ∖ ℕ)} = d$
63	36 61 62	3syl	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to {d ↾}_{(ℤ ∖ ℕ)} = d$
64	60 63	syl5eq	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = d$
65	64	3ad2ant3	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = d$
66	59 65	uneq12d	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \circ ({I ↾}_{(ℤ ∖ ℕ)})) \cup (d \circ ({I ↾}_{(ℤ ∖ ℕ)})) = \emptyset \cup d$
67	51 66	syl5eq	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset \cup d$
68		uncom	$⊢ \emptyset \cup d = d \cup \emptyset$
69		un0	$⊢ d \cup \emptyset = d$
70	68 69	eqtri	$⊢ \emptyset \cup d = d$
71	67 70	eqtrdi	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}) = d$
72	50 71	uneq12d	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to ((a \cup d) \circ F) \cup ((a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)})) = (a \circ F) \cup d$
73	34 72	syl5req	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \circ F) \cup d = (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))$
74	31 32 33 73	syl3anc	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (a \circ F) \cup d = (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))$
75	74	fveq2d	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to b ((a \circ F) \cup d) = b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))$
76		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
77		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))} \subseteq ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
78	1 76 77	mp2an	$⊢ {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))} \subseteq ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
79	42	reseq2i	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {a ↾}_{\emptyset}$
80		res0	$⊢ {a ↾}_{\emptyset} = \emptyset$
81	79 80	eqtri	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = \emptyset$
82	42	reseq2i	$⊢ {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{\emptyset}$
83		res0	$⊢ {d ↾}_{\emptyset} = \emptyset$
84	82 83	eqtri	$⊢ {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = \emptyset$
85	81 84	eqtr4i	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))}$
86		elmapresaun	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \land {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))}) \to a \cup d \in ({ℕ_{0}}^{((1 \dots M) \cup (ℤ ∖ ℕ))})$
87		uncom	$⊢ (1 \dots M) \cup (ℤ ∖ ℕ) = (ℤ ∖ ℕ) \cup (1 \dots M)$
88	87	oveq2i	$⊢ {ℕ_{0}}^{((1 \dots M) \cup (ℤ ∖ ℕ))} = {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
89	86 88	eleqtrdi	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \land {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))}) \to a \cup d \in ({ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
90	85 89	mp3an3	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \cup d \in ({ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
91	78 90	sseldi	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \cup d \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
92	91	adantll	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \cup d \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
93		coeq1	$⊢ e = a \cup d \to e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) = (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))$
94	93	fveq2d	$⊢ e = a \cup d \to b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))) = b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))$
95		eqid	$⊢ (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) = (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))))$
96		fvex	$⊢ b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))) \in V$
97	94 95 96	fvmpt	$⊢ a \cup d \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) \to (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))$
98	92 97	syl	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))$
99	75 98	eqtr4d	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to b ((a \circ F) \cup d) = (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d)$
100	99	eqeq1d	$⊢ (((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to (b ((a \circ F) \cup d) = 0 \leftrightarrow (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0)$
101	100	rexbidva	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to (\exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b ((a \circ F) \cup d) = 0 \leftrightarrow \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0)$
102	30 101	bitrd	$⊢ ((((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \land a \in ({ℕ_{0}}^{(1 \dots M)})) \to (a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \leftrightarrow \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0)$
103	102	rabbidva	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\}\} = \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0\}$
104		simplll	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to M \in ℕ_{0}$
105		ovex	$⊢ (1 \dots M) \in V$
106	3 105	unex	$⊢ (ℤ ∖ ℕ) \cup (1 \dots M) \in V$
107	106	a1i	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to (ℤ ∖ ℕ) \cup (1 \dots M) \in V$
108		simpr	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))$
109	56	a1i	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
110		id	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to F : (1 \dots N) ⟶ (1 \dots M)$
111		incom	$⊢ (ℤ ∖ ℕ) \cap (1 \dots N) = (1 \dots N) \cap (ℤ ∖ ℕ)$
112		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
113		ssdisj	$⊢ ((1 \dots N) \subseteq ℕ \land ℕ \cap (ℤ ∖ ℕ) = \emptyset) \to (1 \dots N) \cap (ℤ ∖ ℕ) = \emptyset$
114	112 18 113	mp2an	$⊢ (1 \dots N) \cap (ℤ ∖ ℕ) = \emptyset$
115	111 114	eqtri	$⊢ (ℤ ∖ ℕ) \cap (1 \dots N) = \emptyset$
116	115	a1i	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (ℤ ∖ ℕ) \cap (1 \dots N) = \emptyset$
117		fun	$⊢ ((({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ \land F : (1 \dots N) ⟶ (1 \dots M)) \land (ℤ ∖ ℕ) \cap (1 \dots N) = \emptyset) \to (({I ↾}_{(ℤ ∖ ℕ)}) \cup F) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
118	109 110 116 117	syl21anc	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (({I ↾}_{(ℤ ∖ ℕ)}) \cup F) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
119		uncom	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) \cup F = F \cup ({I ↾}_{(ℤ ∖ ℕ)})$
120	119	feq1i	$⊢ (({I ↾}_{(ℤ ∖ ℕ)}) \cup F) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M) \leftrightarrow (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
121	118 120	sylib	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
122	121	ad3antlr	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
123		mzprename	$⊢ ((ℤ ∖ ℕ) \cup (1 \dots M) \in V \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N)) \land (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)) \to (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots M))$
124	107 108 122 123	syl3anc	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots M))$
125	3 16 19	eldioph4i	$⊢ (M \in ℕ_{0} \land (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots M))) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0\} \in Dioph (M)$
126	104 124 125	syl2anc	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) (e \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}) ⟼ b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))) (a \cup d) = 0\} \in Dioph (M)$
127	103 126	eqeltrd	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\}\} \in Dioph (M)$
128		eleq2	$⊢ S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \to (a \circ F \in S \leftrightarrow a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\})$
129	128	rabbidv	$⊢ S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} = \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\}\}$
130	129	eleq1d	$⊢ S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \to (\{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M) \leftrightarrow \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\}\} \in Dioph (M))$
131	127 130	syl5ibrcom	$⊢ (((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \land b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N))) \to (S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M))$
132	131	rexlimdva	$⊢ ((M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \land N \in ℕ_{0}) \to (\exists b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N)) S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\} \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M))$
133	132	expimpd	$⊢ (M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \to ((N \in ℕ_{0} \land \exists b \in mzPoly ((ℤ ∖ ℕ) \cup (1 \dots N)) S = \{c \in ({ℕ_{0}}^{(1 \dots N)}) \| \exists d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) b (c \cup d) = 0\}) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M))$
134	20 133	syl5bi	$⊢ (M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \to (S \in Dioph (N) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M))$
135	134	impcom	$⊢ (S \in Dioph (N) \land (M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M))) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M)$
136	135	3impb	$⊢ (S \in Dioph (N) \land M \in ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M)) \to \{a \in ({ℕ_{0}}^{(1 \dots M)}) \| a \circ F \in S\} \in Dioph (M)$

Metamath Proof Explorer

Theorem diophren

Proof