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	$$⊢\underset{\dot{}}{0}=0_P$$
	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 {\mathbb{N}}_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	$$⊢\underset{\dot{}}{0}=0_P$$
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 {\mathbb{N}}_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 {\mathbb{N}}_0\to \left(D\left(F\right)=X\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
16	9 15	syl	$$⊢\phi \to \left(D\left(F\right)=X\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
17	16	imp	$$⊢\left(\phi \wedge D\left(F\right)=X\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
18	1 2 3 4	deg1nn0clb	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\right)\to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
19	7 8 18	syl2anc	$$⊢\phi \to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
20	19	adantr	$$⊢\left(\phi \wedge D\left(F\right)=X\right)\to \left(F\ne \underset{\dot{}}{0}\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
21	17 20	mpbird	$$⊢\left(\phi \wedge D\left(F\right)=X\right)\to F\ne \underset{\dot{}}{0}$$
22	1 2 3 4 5 6	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to A\left(D\left(F\right)\right)\ne Y$$
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$$