Theorem q1pcl

Description: Closure of the quotient by a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	q1pcl.q	|- Q = ( quot1p ` R )
	q1pcl.p	|- P = ( Poly1 ` R )
	q1pcl.b	|- B = ( Base ` P )
	q1pcl.c	|- C = ( Unic1p ` R )
Assertion	q1pcl	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )

Proof

Step	Hyp	Ref	Expression
1		q1pcl.q	|- Q = ( quot1p ` R )
2		q1pcl.p	|- P = ( Poly1 ` R )
3		q1pcl.b	|- B = ( Base ` P )
4		q1pcl.c	|- C = ( Unic1p ` R )
5		eqid	|- ( F Q G ) = ( F Q G )
6		eqid	|- ( deg1 ` R ) = ( deg1 ` R )
7		eqid	|- ( -g ` P ) = ( -g ` P )
8		eqid	|- ( .r ` P ) = ( .r ` P )
9	1 2 3 6 7 8 4	q1peqb	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( ( F Q G ) e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( ( F Q G ) ( .r ` P ) G ) ) ) < ( ( deg1 ` R ) ` G ) ) <-> ( F Q G ) = ( F Q G ) ) )
10	5 9	mpbiri	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F Q G ) e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( ( F Q G ) ( .r ` P ) G ) ) ) < ( ( deg1 ` R ) ` G ) ) )
11	10	simpld	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )