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 = ( Poly1 ` R )
	ply1divalg.d	|- D = ( deg1 ` R )
	ply1divalg.b	|- B = ( Base ` P )
	ply1divalg.m	|- .- = ( -g ` P )
	ply1divalg.z	|- .0. = ( 0g ` P )
	ply1divalg.t	|- .xb = ( .r ` P )
	ply1divalg.r1	|- ( ph -> R e. Ring )
	ply1divalg.f	|- ( ph -> F e. B )
	ply1divalg.g1	|- ( ph -> G e. B )
	ply1divalg.g2	|- ( ph -> G =/= .0. )
	ply1divalg.g3	|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. U )
	ply1divalg.u	|- U = ( Unit ` R )
Assertion	ply1divalg	|- ( ph -> E! q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )

Proof

Step	Hyp	Ref	Expression
1		ply1divalg.p	|- P = ( Poly1 ` R )
2		ply1divalg.d	|- D = ( deg1 ` R )
3		ply1divalg.b	|- B = ( Base ` P )
4		ply1divalg.m	|- .- = ( -g ` P )
5		ply1divalg.z	|- .0. = ( 0g ` P )
6		ply1divalg.t	|- .xb = ( .r ` P )
7		ply1divalg.r1	|- ( ph -> R e. Ring )
8		ply1divalg.f	|- ( ph -> F e. B )
9		ply1divalg.g1	|- ( ph -> G e. B )
10		ply1divalg.g2	|- ( ph -> G =/= .0. )
11		ply1divalg.g3	|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. U )
12		ply1divalg.u	|- U = ( Unit ` R )
13		eqid	|- ( 1r ` R ) = ( 1r ` R )
14		eqid	|- ( Base ` R ) = ( Base ` R )
15		eqid	|- ( .r ` R ) = ( .r ` R )
16		eqid	|- ( invr ` R ) = ( invr ` R )
17	12 16 14	ringinvcl	|- ( ( R e. Ring /\ ( ( coe1 ` G ) ` ( D ` G ) ) e. U ) -> ( ( invr ` R ) ` ( ( coe1 ` G ) ` ( D ` G ) ) ) e. ( Base ` R ) )
18	7 11 17	syl2anc	|- ( ph -> ( ( invr ` R ) ` ( ( coe1 ` G ) ` ( D ` G ) ) ) e. ( Base ` R ) )
19	12 16 15 13	unitrinv	|- ( ( R e. Ring /\ ( ( coe1 ` G ) ` ( D ` G ) ) e. U ) -> ( ( ( coe1 ` G ) ` ( D ` G ) ) ( .r ` R ) ( ( invr ` R ) ` ( ( coe1 ` G ) ` ( D ` G ) ) ) ) = ( 1r ` R ) )
20	7 11 19	syl2anc	|- ( ph -> ( ( ( coe1 ` G ) ` ( D ` G ) ) ( .r ` R ) ( ( invr ` R ) ` ( ( coe1 ` G ) ` ( D ` G ) ) ) ) = ( 1r ` R ) )
21	1 2 3 4 5 6 7 8 9 10 13 14 15 18 20	ply1divex	|- ( ph -> E. q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
22		eqid	|- ( RLReg ` R ) = ( RLReg ` R )
23	22 12	unitrrg	|- ( R e. Ring -> U C_ ( RLReg ` R ) )
24	7 23	syl	|- ( ph -> U C_ ( RLReg ` R ) )
25	24 11	sseldd	|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( RLReg ` R ) )
26	1 2 3 4 5 6 7 8 9 10 25 22	ply1divmo	|- ( ph -> E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )
27		reu5	|- ( E! q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) <-> ( E. q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) /\ E* q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) ) )
28	21 26 27	sylanbrc	|- ( ph -> E! q e. B ( D ` ( F .- ( G .xb q ) ) ) < ( D ` G ) )