Theorem deg1submon1p

Description: The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1submon1p.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1submon1p.o	$$⊢O={Monic}_{\mathrm{1p}}\left(R\right)$$
	deg1submon1p.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1submon1p.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	deg1submon1p.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1submon1p.f1	$$⊢\phi \to F\in O$$
	deg1submon1p.f2	$$⊢\phi \to D\left(F\right)=X$$
	deg1submon1p.g1	$$⊢\phi \to G\in O$$
	deg1submon1p.g2	$$⊢\phi \to D\left(G\right)=X$$
Assertion	deg1submon1p	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)<X$$

Proof

Step	Hyp	Ref	Expression
1		deg1submon1p.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1submon1p.o	$$⊢O={Monic}_{\mathrm{1p}}\left(R\right)$$
3		deg1submon1p.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
4		deg1submon1p.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		deg1submon1p.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		deg1submon1p.f1	$$⊢\phi \to F\in O$$
7		deg1submon1p.f2	$$⊢\phi \to D\left(F\right)=X$$
8		deg1submon1p.g1	$$⊢\phi \to G\in O$$
9		deg1submon1p.g2	$$⊢\phi \to D\left(G\right)=X$$
10		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
11	3 10 2	mon1pcl	$$⊢F\in O\to F\in {\mathrm{Base}}_P$$
12	6 11	syl	$$⊢\phi \to F\in {\mathrm{Base}}_P$$
13		eqid	$$⊢0_P=0_P$$
14	3 13 2	mon1pn0	$$⊢F\in O\to F\ne 0_P$$
15	6 14	syl	$$⊢\phi \to F\ne 0_P$$
16	1 3 13 10	deg1nn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in {\mathrm{Base}}_P\wedge F\ne 0_P\right)\to D\left(F\right)\in {\mathbb{N}}_0$$
17	5 12 15 16	syl3anc	$$⊢\phi \to D\left(F\right)\in {\mathbb{N}}_0$$
18	7 17	eqeltrrd	$$⊢\phi \to X\in {\mathbb{N}}_0$$
19	18	nn0red	$$⊢\phi \to X\in ℝ$$
20	19	leidd	$$⊢\phi \to X\le X$$
21	7 20	eqbrtrd	$$⊢\phi \to D\left(F\right)\le X$$
22	3 10 2	mon1pcl	$$⊢G\in O\to G\in {\mathrm{Base}}_P$$
23	8 22	syl	$$⊢\phi \to G\in {\mathrm{Base}}_P$$
24	9 20	eqbrtrd	$$⊢\phi \to D\left(G\right)\le X$$
25		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
26		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
27	7	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)={\mathrm{coe}}_1\left(F\right)\left(X\right)$$
28		eqid	$$⊢1_R=1_R$$
29	1 28 2	mon1pldg	$$⊢F\in O\to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=1_R$$
30	6 29	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(D\left(F\right)\right)=1_R$$
31	27 30	eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(X\right)=1_R$$
32	1 28 2	mon1pldg	$$⊢G\in O\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=1_R$$
33	8 32	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)=1_R$$
34	9	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)={\mathrm{coe}}_1\left(G\right)\left(X\right)$$
35	31 33 34	3eqtr2d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(X\right)={\mathrm{coe}}_1\left(G\right)\left(X\right)$$
36	1 3 10 4 18 5 12 21 23 24 25 26 35	deg1sublt	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)<X$$