# Metamath Proof Explorer

## Theorem 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

### Proof

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