rabdiophlem2

Description: Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014)

		Ref	Expression
	Hypothesis	rabdiophlem2.1	$⊢ M = N + 1$
	Assertion	rabdiophlem2	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots M)}) ⟼ ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A) \in mzPoly ((1 \dots M))$

Proof

Step	Hyp	Ref	Expression
1		rabdiophlem2.1	$⊢ M = N + 1$
2		nfcv	$⊢ \underline{Ⅎ} a A$
3		nfcsb1v	$⊢ \underline{Ⅎ} u ⦋ a / u ⦌ A$
4		csbeq1a	$⊢ u = a \to A = ⦋ a / u ⦌ A$
5	2 3 4	cbvmpt	$⊢ (u \in (ℤ^{(1 \dots N)}) ⟼ A) = (a \in (ℤ^{(1 \dots N)}) ⟼ ⦋ a / u ⦌ A)$
6	5	fveq1i	$⊢ (u \in (ℤ^{(1 \dots N)}) ⟼ A) ({t ↾}_{(1 \dots N)}) = (a \in (ℤ^{(1 \dots N)}) ⟼ ⦋ a / u ⦌ A) ({t ↾}_{(1 \dots N)})$
7		eqid	$⊢ (a \in (ℤ^{(1 \dots N)}) ⟼ ⦋ a / u ⦌ A) = (a \in (ℤ^{(1 \dots N)}) ⟼ ⦋ a / u ⦌ A)$
8		csbeq1	$⊢ a = {t ↾}_{(1 \dots N)} \to ⦋ a / u ⦌ A = ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A$
9	1	mapfzcons1cl	$⊢ t \in (ℤ^{(1 \dots M)}) \to {t ↾}_{(1 \dots N)} \in (ℤ^{(1 \dots N)})$
10	9	adantl	$⊢ ((N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in (ℤ^{(1 \dots M)})) \to {t ↾}_{(1 \dots N)} \in (ℤ^{(1 \dots N)})$
11		mzpf	$⊢ (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to (u \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
12		eqid	$⊢ (u \in (ℤ^{(1 \dots N)}) ⟼ A) = (u \in (ℤ^{(1 \dots N)}) ⟼ A)$
13	12	fmpt	$⊢ \forall u \in (ℤ^{(1 \dots N)}) A \in ℤ \leftrightarrow (u \in (ℤ^{(1 \dots N)}) ⟼ A) : ℤ^{(1 \dots N)} ⟶ ℤ$
14	11 13	sylibr	$⊢ (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N)) \to \forall u \in (ℤ^{(1 \dots N)}) A \in ℤ$
15	14	ad2antlr	$⊢ ((N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in (ℤ^{(1 \dots M)})) \to \forall u \in (ℤ^{(1 \dots N)}) A \in ℤ$
16		nfcsb1v	$⊢ \underline{Ⅎ} u ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A$
17	16	nfel1	$⊢ Ⅎ u ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A \in ℤ$
18		csbeq1a	$⊢ u = {t ↾}_{(1 \dots N)} \to A = ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A$
19	18	eleq1d	$⊢ u = {t ↾}_{(1 \dots N)} \to (A \in ℤ \leftrightarrow ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A \in ℤ)$
20	17 19	rspc	$⊢ {t ↾}_{(1 \dots N)} \in (ℤ^{(1 \dots N)}) \to (\forall u \in (ℤ^{(1 \dots N)}) A \in ℤ \to ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A \in ℤ)$
21	10 15 20	sylc	$⊢ ((N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in (ℤ^{(1 \dots M)})) \to ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A \in ℤ$
22	7 8 10 21	fvmptd3	$⊢ ((N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in (ℤ^{(1 \dots M)})) \to (a \in (ℤ^{(1 \dots N)}) ⟼ ⦋ a / u ⦌ A) ({t ↾}_{(1 \dots N)}) = ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A$
23	6 22	syl5req	$⊢ ((N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \land t \in (ℤ^{(1 \dots M)})) \to ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A = (u \in (ℤ^{(1 \dots N)}) ⟼ A) ({t ↾}_{(1 \dots N)})$
24	23	mpteq2dva	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots M)}) ⟼ ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A) = (t \in (ℤ^{(1 \dots M)}) ⟼ (u \in (ℤ^{(1 \dots N)}) ⟼ A) ({t ↾}_{(1 \dots N)}))$
25		ovexd	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (1 \dots M) \in V$
26		fzssp1	$⊢ (1 \dots N) \subseteq (1 \dots N + 1)$
27	1	oveq2i	$⊢ (1 \dots M) = (1 \dots N + 1)$
28	26 27	sseqtrri	$⊢ (1 \dots N) \subseteq (1 \dots M)$
29	28	a1i	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (1 \dots N) \subseteq (1 \dots M)$
30		simpr	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))$
31		mzpresrename	$⊢ ((1 \dots M) \in V \land (1 \dots N) \subseteq (1 \dots M) \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots M)}) ⟼ (u \in (ℤ^{(1 \dots N)}) ⟼ A) ({t ↾}_{(1 \dots N)})) \in mzPoly ((1 \dots M))$
32	25 29 30 31	syl3anc	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots M)}) ⟼ (u \in (ℤ^{(1 \dots N)}) ⟼ A) ({t ↾}_{(1 \dots N)})) \in mzPoly ((1 \dots M))$
33	24 32	eqeltrd	$⊢ (N \in ℕ_{0} \land (u \in (ℤ^{(1 \dots N)}) ⟼ A) \in mzPoly ((1 \dots N))) \to (t \in (ℤ^{(1 \dots M)}) ⟼ ⦋ ({t ↾}_{(1 \dots N)}) / u ⦌ A) \in mzPoly ((1 \dots M))$

Metamath Proof Explorer

Theorem rabdiophlem2

Proof