# Metamath Proof Explorer

## Theorem deg1ldgn

Description: An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses deg1z.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
deg1z.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
deg1z.z
deg1nn0cl.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
deg1ldg.y ${⊢}{Y}={0}_{{R}}$
deg1ldg.a ${⊢}{A}={\mathrm{coe}}_{1}\left({F}\right)$
deg1ldgn.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
deg1ldgn.f ${⊢}{\phi }\to {F}\in {B}$
deg1ldgn.x ${⊢}{\phi }\to {X}\in {ℕ}_{0}$
deg1ldgn.e ${⊢}{\phi }\to {A}\left({X}\right)={Y}$
Assertion deg1ldgn ${⊢}{\phi }\to {D}\left({F}\right)\ne {X}$

### Proof

Step Hyp Ref Expression
1 deg1z.d ${⊢}{D}={\mathrm{deg}}_{1}\left({R}\right)$
2 deg1z.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 deg1z.z
4 deg1nn0cl.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
5 deg1ldg.y ${⊢}{Y}={0}_{{R}}$
6 deg1ldg.a ${⊢}{A}={\mathrm{coe}}_{1}\left({F}\right)$
7 deg1ldgn.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
8 deg1ldgn.f ${⊢}{\phi }\to {F}\in {B}$
9 deg1ldgn.x ${⊢}{\phi }\to {X}\in {ℕ}_{0}$
10 deg1ldgn.e ${⊢}{\phi }\to {A}\left({X}\right)={Y}$
11 fveq2 ${⊢}{D}\left({F}\right)={X}\to {A}\left({D}\left({F}\right)\right)={A}\left({X}\right)$
12 11 adantl ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {A}\left({D}\left({F}\right)\right)={A}\left({X}\right)$
13 7 adantr ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {R}\in \mathrm{Ring}$
14 8 adantr ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {F}\in {B}$
15 eleq1a ${⊢}{X}\in {ℕ}_{0}\to \left({D}\left({F}\right)={X}\to {D}\left({F}\right)\in {ℕ}_{0}\right)$
16 9 15 syl ${⊢}{\phi }\to \left({D}\left({F}\right)={X}\to {D}\left({F}\right)\in {ℕ}_{0}\right)$
17 16 imp ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {D}\left({F}\right)\in {ℕ}_{0}$
18 1 2 3 4 deg1nn0clb
19 7 8 18 syl2anc
23 13 14 21 22 syl3anc ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {A}\left({D}\left({F}\right)\right)\ne {Y}$
24 12 23 eqnetrrd ${⊢}\left({\phi }\wedge {D}\left({F}\right)={X}\right)\to {A}\left({X}\right)\ne {Y}$
25 24 ex ${⊢}{\phi }\to \left({D}\left({F}\right)={X}\to {A}\left({X}\right)\ne {Y}\right)$
26 25 necon2d ${⊢}{\phi }\to \left({A}\left({X}\right)={Y}\to {D}\left({F}\right)\ne {X}\right)$
27 10 26 mpd ${⊢}{\phi }\to {D}\left({F}\right)\ne {X}$