Theorem ply1divalg

Description: The division algorithm for univariate polynomials over a ring. For polynomials F , G such that G =/= 0 and the leading coefficient of G is a unit, there are unique polynomials q and r = F - ( G x. q ) such that the degree of r is less than the degree of G . (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Hypotheses	ply1divalg.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
	ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
	ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
	ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
	ply1divalg.f	$$⊢\phi \to F\in B$$
	ply1divalg.g1	$$⊢\phi \to G\in B$$
	ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
	ply1divalg.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U$$
	ply1divalg.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
Assertion	ply1divalg	$$⊢\phi \to \exists !q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1divalg.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
3		ply1divalg.b	$$⊢B={\mathrm{Base}}_P$$
4		ply1divalg.m	$$⊢\underset{\dot{}}{-}={-}_P$$
5		ply1divalg.z	$$⊢\underset{\dot{}}{0}=0_P$$
6		ply1divalg.t	$$⊢\underset{\dot{}}{\bullet }={\cdot }_P$$
7		ply1divalg.r1	$$⊢\phi \to R\in \mathrm{Ring}$$
8		ply1divalg.f	$$⊢\phi \to F\in B$$
9		ply1divalg.g1	$$⊢\phi \to G\in B$$
10		ply1divalg.g2	$$⊢\phi \to G\ne \underset{\dot{}}{0}$$
11		ply1divalg.g3	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U$$
12		ply1divalg.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
13		eqid	$$⊢1_R=1_R$$
14		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
15		eqid	$$⊢{\cdot }_R={\cdot }_R$$
16		eqid	$$⊢{inv}_r\left(R\right)={inv}_r\left(R\right)$$
17	12 16 14	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U\right)\to {inv}_r\left(R\right)\left({\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\right)\in {\mathrm{Base}}_R$$
18	7 11 17	syl2anc	$$⊢\phi \to {inv}_r\left(R\right)\left({\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\right)\in {\mathrm{Base}}_R$$
19	12 16 15 13	unitrinv	$$⊢\left(R\in \mathrm{Ring}\wedge {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in U\right)\to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right){\cdot }_R{inv}_r\left(R\right)\left({\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\right)=1_R$$
20	7 11 19	syl2anc	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right){\cdot }_R{inv}_r\left(R\right)\left({\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\right)=1_R$$
21	1 2 3 4 5 6 7 8 9 10 13 14 15 18 20	ply1divex	$$⊢\phi \to \exists q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$
22		eqid	$$⊢\mathrm{RLReg}\left(R\right)=\mathrm{RLReg}\left(R\right)$$
23	22 12	unitrrg	$$⊢R\in \mathrm{Ring}\to U\subseteq \mathrm{RLReg}\left(R\right)$$
24	7 23	syl	$$⊢\phi \to U\subseteq \mathrm{RLReg}\left(R\right)$$
25	24 11	sseldd	$$⊢\phi \to {\mathrm{coe}}_1\left(G\right)\left(D\left(G\right)\right)\in \mathrm{RLReg}\left(R\right)$$
26	1 2 3 4 5 6 7 8 9 10 25 22	ply1divmo	$$⊢\phi \to {\exists }^{*}q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$
27		reu5	$$⊢\exists !q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\leftrightarrow \left(\exists q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\wedge {\exists }^{*}q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)\right)$$
28	21 26 27	sylanbrc	$$⊢\phi \to \exists !q\in BD\left(F\underset{\dot{}}{-}\left(G\underset{\dot{}}{\bullet }q\right)\right)<D\left(G\right)$$