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		disjdifr	$⊢ (ℤ ∖ ℕ) \cap ℕ = \emptyset$
18	3 16 17	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\})$
19		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)})$
20		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)$
21		ovex	$⊢ (1 \dots N) \in V$
22	21	mapco2	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land F : (1 \dots N) ⟶ (1 \dots M)) \to a \circ F \in ({ℕ_{0}}^{(1 \dots N)})$
23	19 20 22	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)})$
24		uneq1	$⊢ c = a \circ F \to c \cup d = (a \circ F) \cup d$
25	24	fveqeq2d	$⊢ c = a \circ F \to (b (c \cup d) = 0 \leftrightarrow b ((a \circ F) \cup d) = 0)$
26	25	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)$
27	26	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)$
28	23 27	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)$
29		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)$
30		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)})$
31		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}}^{(ℤ ∖ ℕ)})$
32		coundi	$⊢ (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) = ((a \cup d) \circ F) \cup ((a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}))$
33		coundir	$⊢ (a \cup d) \circ F = (a \circ F) \cup (d \circ F)$
34		elmapi	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to d : ℤ ∖ ℕ ⟶ ℕ_{0}$
35	34	3ad2ant3	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d : ℤ ∖ ℕ ⟶ ℕ_{0}$
36		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)$
37		incom	$⊢ (ℤ ∖ ℕ) \cap (1 \dots M) = (1 \dots M) \cap (ℤ ∖ ℕ)$
38		fz1ssnn	$⊢ (1 \dots M) \subseteq ℕ$
39		disjdif	$⊢ ℕ \cap (ℤ ∖ ℕ) = \emptyset$
40		ssdisj	$⊢ ((1 \dots M) \subseteq ℕ \land ℕ \cap (ℤ ∖ ℕ) = \emptyset) \to (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset$
41	38 39 40	mp2an	$⊢ (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset$
42	37 41	eqtri	$⊢ (ℤ ∖ ℕ) \cap (1 \dots M) = \emptyset$
43	42	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$
44		coeq0i	$⊢ (d : ℤ ∖ ℕ ⟶ ℕ_{0} \land F : (1 \dots N) ⟶ (1 \dots M) \land (ℤ ∖ ℕ) \cap (1 \dots M) = \emptyset) \to d \circ F = \emptyset$
45	35 36 43 44	syl3anc	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d \circ F = \emptyset$
46	45	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$
47	33 46	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$
48		un0	$⊢ (a \circ F) \cup \emptyset = a \circ F$
49	47 48	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$
50		coundir	$⊢ (a \cup d) \circ ({I ↾}_{(ℤ ∖ ℕ)}) = (a \circ ({I ↾}_{(ℤ ∖ ℕ)})) \cup (d \circ ({I ↾}_{(ℤ ∖ ℕ)}))$
51		elmapi	$⊢ a \in ({ℕ_{0}}^{(1 \dots M)}) \to a : (1 \dots M) ⟶ ℕ_{0}$
52	51	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}$
53		f1oi	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ \underset{1-1 onto}{⟶} ℤ ∖ ℕ$
54		f1of	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ \underset{1-1 onto}{⟶} ℤ ∖ ℕ \to ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
55	53 54	ax-mp	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
56		coeq0i	$⊢ (a : (1 \dots M) ⟶ ℕ_{0} \land ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ \land (1 \dots M) \cap (ℤ ∖ ℕ) = \emptyset) \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
57	55 41 56	mp3an23	$⊢ a : (1 \dots M) ⟶ ℕ_{0} \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
58	52 57	syl	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \circ ({I ↾}_{(ℤ ∖ ℕ)}) = \emptyset$
59		coires1	$⊢ d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = {d ↾}_{(ℤ ∖ ℕ)}$
60		ffn	$⊢ d : ℤ ∖ ℕ ⟶ ℕ_{0} \to d Fn (ℤ ∖ ℕ)$
61		fnresdm	$⊢ d Fn (ℤ ∖ ℕ) \to {d ↾}_{(ℤ ∖ ℕ)} = d$
62	34 60 61	3syl	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to {d ↾}_{(ℤ ∖ ℕ)} = d$
63	59 62	syl5eq	$⊢ d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)}) \to d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = d$
64	63	3ad2ant3	$⊢ (F : (1 \dots N) ⟶ (1 \dots M) \land a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to d \circ ({I ↾}_{(ℤ ∖ ℕ)}) = d$
65	58 64	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$
66	50 65	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$
67		uncom	$⊢ \emptyset \cup d = d \cup \emptyset$
68		un0	$⊢ d \cup \emptyset = d$
69	67 68	eqtri	$⊢ \emptyset \cup d = d$
70	66 69	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$
71	49 70	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$
72	32 71	eqtr2id	$⊢ (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 ↾}_{(ℤ ∖ ℕ)}))$
73	29 30 31 72	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 ↾}_{(ℤ ∖ ℕ)}))$
74	73	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 ↾}_{(ℤ ∖ ℕ)})))$
75		nn0ssz	$⊢ ℕ_{0} \subseteq ℤ$
76		mapss	$⊢ (ℤ \in V \land ℕ_{0} \subseteq ℤ) \to {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))} \subseteq ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
77	1 75 76	mp2an	$⊢ {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))} \subseteq ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
78	41	reseq2i	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {a ↾}_{\emptyset}$
79		res0	$⊢ {a ↾}_{\emptyset} = \emptyset$
80	78 79	eqtri	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = \emptyset$
81	41	reseq2i	$⊢ {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{\emptyset}$
82		res0	$⊢ {d ↾}_{\emptyset} = \emptyset$
83	81 82	eqtri	$⊢ {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = \emptyset$
84	80 83	eqtr4i	$⊢ {a ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))} = {d ↾}_{((1 \dots M) \cap (ℤ ∖ ℕ))}$
85		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 (ℤ ∖ ℕ))})$
86		uncom	$⊢ (1 \dots M) \cup (ℤ ∖ ℕ) = (ℤ ∖ ℕ) \cup (1 \dots M)$
87	86	oveq2i	$⊢ {ℕ_{0}}^{((1 \dots M) \cup (ℤ ∖ ℕ))} = {ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))}$
88	85 87	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))})$
89	84 88	mp3an3	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \cup d \in ({ℕ_{0}}^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
90	77 89	sseldi	$⊢ (a \in ({ℕ_{0}}^{(1 \dots M)}) \land d \in ({ℕ_{0}}^{(ℤ ∖ ℕ)})) \to a \cup d \in (ℤ^{((ℤ ∖ ℕ) \cup (1 \dots M))})$
91	90	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))})$
92		coeq1	$⊢ e = a \cup d \to e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) = (a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))$
93	92	fveq2d	$⊢ e = a \cup d \to b (e \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))) = b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)})))$
94		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 ↾}_{(ℤ ∖ ℕ)}))))$
95		fvex	$⊢ b ((a \cup d) \circ (F \cup ({I ↾}_{(ℤ ∖ ℕ)}))) \in V$
96	93 94 95	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 ↾}_{(ℤ ∖ ℕ)})))$
97	91 96	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 ↾}_{(ℤ ∖ ℕ)})))$
98	74 97	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)$
99	98	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)$
100	99	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)$
101	28 100	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)$
102	101	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\}$
103		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}$
104		ovex	$⊢ (1 \dots M) \in V$
105	3 104	unex	$⊢ (ℤ ∖ ℕ) \cup (1 \dots M) \in V$
106	105	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$
107		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))$
108	55	a1i	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to ({I ↾}_{(ℤ ∖ ℕ)}) : ℤ ∖ ℕ ⟶ ℤ ∖ ℕ$
109		id	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to F : (1 \dots N) ⟶ (1 \dots M)$
110		incom	$⊢ (ℤ ∖ ℕ) \cap (1 \dots N) = (1 \dots N) \cap (ℤ ∖ ℕ)$
111		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
112		ssdisj	$⊢ ((1 \dots N) \subseteq ℕ \land ℕ \cap (ℤ ∖ ℕ) = \emptyset) \to (1 \dots N) \cap (ℤ ∖ ℕ) = \emptyset$
113	111 39 112	mp2an	$⊢ (1 \dots N) \cap (ℤ ∖ ℕ) = \emptyset$
114	110 113	eqtri	$⊢ (ℤ ∖ ℕ) \cap (1 \dots N) = \emptyset$
115	114	a1i	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (ℤ ∖ ℕ) \cap (1 \dots N) = \emptyset$
116		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)$
117	108 109 115 116	syl21anc	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (({I ↾}_{(ℤ ∖ ℕ)}) \cup F) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
118		uncom	$⊢ ({I ↾}_{(ℤ ∖ ℕ)}) \cup F = F \cup ({I ↾}_{(ℤ ∖ ℕ)})$
119	118	feq1i	$⊢ (({I ↾}_{(ℤ ∖ ℕ)}) \cup F) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M) \leftrightarrow (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
120	117 119	sylib	$⊢ F : (1 \dots N) ⟶ (1 \dots M) \to (F \cup ({I ↾}_{(ℤ ∖ ℕ)})) : (ℤ ∖ ℕ) \cup (1 \dots N) ⟶ (ℤ ∖ ℕ) \cup (1 \dots M)$
121	120	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)$
122		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))$
123	106 107 121 122	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))$
124	3 16 17	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)$
125	103 123 124	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)$
126	102 125	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)$
127		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\})$
128	127	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\}\}$
129	128	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))$
130	126 129	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))$
131	130	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))$
132	131	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))$
133	18 132	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))$
134	133	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)$
135	134	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