Theorem deg1sublt

Description: Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015)

	Ref	Expression
Hypotheses	deg1sublt.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1sublt.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1sublt.b	$$⊢B={\mathrm{Base}}_P$$
	deg1sublt.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	deg1sublt.l	$$⊢\phi \to L\in {\mathbb{N}}_0$$
	deg1sublt.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	deg1sublt.fb	$$⊢\phi \to F\in B$$
	deg1sublt.fd	$$⊢\phi \to D\left(F\right)\le L$$
	deg1sublt.gb	$$⊢\phi \to G\in B$$
	deg1sublt.gd	$$⊢\phi \to D\left(G\right)\le L$$
	deg1sublt.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
	deg1sublt.c	$$⊢C={\mathrm{coe}}_1\left(G\right)$$
	deg1sublt.eq	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(L\right)={\mathrm{coe}}_1\left(G\right)\left(L\right)$$
Assertion	deg1sublt	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)<L$$

Proof

Step	Hyp	Ref	Expression
1		deg1sublt.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1sublt.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1sublt.b	$$⊢B={\mathrm{Base}}_P$$
4		deg1sublt.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		deg1sublt.l	$$⊢\phi \to L\in {\mathbb{N}}_0$$
6		deg1sublt.r	$$⊢\phi \to R\in \mathrm{Ring}$$
7		deg1sublt.fb	$$⊢\phi \to F\in B$$
8		deg1sublt.fd	$$⊢\phi \to D\left(F\right)\le L$$
9		deg1sublt.gb	$$⊢\phi \to G\in B$$
10		deg1sublt.gd	$$⊢\phi \to D\left(G\right)\le L$$
11		deg1sublt.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
12		deg1sublt.c	$$⊢C={\mathrm{coe}}_1\left(G\right)$$
13		deg1sublt.eq	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(L\right)={\mathrm{coe}}_1\left(G\right)\left(L\right)$$
14		eqid	$$⊢0_P=0_P$$
15		eqid	$$⊢0_R=0_R$$
16		eqid	$$⊢{\mathrm{coe}}_1\left(F\underset{\dot{}}{-}G\right)={\mathrm{coe}}_1\left(F\underset{\dot{}}{-}G\right)$$
17	2	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
18		ringgrp	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{Grp}$$
19	6 17 18	3syl	$$⊢\phi \to P\in \mathrm{Grp}$$
20	3 4	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{-}G\in B$$
21	19 7 9 20	syl3anc	$$⊢\phi \to F\underset{\dot{}}{-}G\in B$$
22		eqid	$$⊢{-}_R={-}_R$$
23	2 3 4 22	coe1subfv	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\wedge L\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{-}G\right)\left(L\right)={\mathrm{coe}}_1\left(F\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)$$
24	6 7 9 5 23	syl31anc	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{-}G\right)\left(L\right)={\mathrm{coe}}_1\left(F\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)$$
25	13	oveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(F\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)={\mathrm{coe}}_1\left(G\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)$$
26		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
27	6 26	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
28		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
29		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
30	28 3 2 29	coe1f	$$⊢G\in B\to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
31	9 30	syl	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right):{\mathbb{N}}_0⟶{\mathrm{Base}}_R$$
32	31 5	ffvelcdmd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(L\right)\in {\mathrm{Base}}_R$$
33	29 15 22	grpsubid	$$⊢\left(R\in \mathrm{Grp}\wedge {\mathrm{coe}}_1\left(G\right)\left(L\right)\in {\mathrm{Base}}_R\right)\to {\mathrm{coe}}_1\left(G\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)=0_R$$
34	27 32 33	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(L\right){-}_R{\mathrm{coe}}_1\left(G\right)\left(L\right)=0_R$$
35	24 25 34	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(F\underset{\dot{}}{-}G\right)\left(L\right)=0_R$$
36	1 2 14 3 15 16 6 21 5 35	deg1ldgn	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\ne L$$
37	36	neneqd	$$⊢\phi \to \neg D\left(F\underset{\dot{}}{-}G\right)=L$$
38	1 2 3	deg1xrcl	$$⊢F\underset{\dot{}}{-}G\in B\to D\left(F\underset{\dot{}}{-}G\right)\in {ℝ}^{*}$$
39	21 38	syl	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\in {ℝ}^{*}$$
40	1 2 3	deg1xrcl	$$⊢G\in B\to D\left(G\right)\in {ℝ}^{*}$$
41	9 40	syl	$$⊢\phi \to D\left(G\right)\in {ℝ}^{*}$$
42	1 2 3	deg1xrcl	$$⊢F\in B\to D\left(F\right)\in {ℝ}^{*}$$
43	7 42	syl	$$⊢\phi \to D\left(F\right)\in {ℝ}^{*}$$
44	41 43	ifcld	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\in {ℝ}^{*}$$
45	5	nn0red	$$⊢\phi \to L\in ℝ$$
46	45	rexrd	$$⊢\phi \to L\in {ℝ}^{*}$$
47	2 1 6 3 4 7 9	deg1suble	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\le if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)$$
48		xrmaxle	$$⊢\left(D\left(F\right)\in {ℝ}^{*}\wedge D\left(G\right)\in {ℝ}^{*}\wedge L\in {ℝ}^{*}\right)\to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L\leftrightarrow \left(D\left(F\right)\le L\wedge D\left(G\right)\le L\right)\right)$$
49	43 41 46 48	syl3anc	$$⊢\phi \to \left(if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L\leftrightarrow \left(D\left(F\right)\le L\wedge D\left(G\right)\le L\right)\right)$$
50	8 10 49	mpbir2and	$$⊢\phi \to if\left(D\left(F\right)\le D\left(G\right),D\left(G\right),D\left(F\right)\right)\le L$$
51	39 44 46 47 50	xrletrd	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)\le L$$
52		xrleloe	$$⊢\left(D\left(F\underset{\dot{}}{-}G\right)\in {ℝ}^{*}\wedge L\in {ℝ}^{*}\right)\to \left(D\left(F\underset{\dot{}}{-}G\right)\le L\leftrightarrow \left(D\left(F\underset{\dot{}}{-}G\right)<L\vee D\left(F\underset{\dot{}}{-}G\right)=L\right)\right)$$
53	39 46 52	syl2anc	$$⊢\phi \to \left(D\left(F\underset{\dot{}}{-}G\right)\le L\leftrightarrow \left(D\left(F\underset{\dot{}}{-}G\right)<L\vee D\left(F\underset{\dot{}}{-}G\right)=L\right)\right)$$
54	51 53	mpbid	$$⊢\phi \to \left(D\left(F\underset{\dot{}}{-}G\right)<L\vee D\left(F\underset{\dot{}}{-}G\right)=L\right)$$
55		orel2	$$⊢\neg D\left(F\underset{\dot{}}{-}G\right)=L\to \left(\left(D\left(F\underset{\dot{}}{-}G\right)<L\vee D\left(F\underset{\dot{}}{-}G\right)=L\right)\to D\left(F\underset{\dot{}}{-}G\right)<L\right)$$
56	37 54 55	sylc	$$⊢\phi \to D\left(F\underset{\dot{}}{-}G\right)<L$$