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 ) )

Metamath Proof Explorer

Theorem ply1divalg

Proof