Theorem r1pcl

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

	Ref	Expression
Hypotheses	r1pval.e	|- E = ( rem1p ` R )
	r1pval.p	|- P = ( Poly1 ` R )
	r1pval.b	|- B = ( Base ` P )
	r1pcl.c	|- C = ( Unic1p ` R )
Assertion	r1pcl	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) e. B )

Proof

Step	Hyp	Ref	Expression
1		r1pval.e	|- E = ( rem1p ` R )
2		r1pval.p	|- P = ( Poly1 ` R )
3		r1pval.b	|- B = ( Base ` P )
4		r1pcl.c	|- C = ( Unic1p ` R )
5		simp2	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> F e. B )
6	2 3 4	uc1pcl	|- ( G e. C -> G e. B )
7	6	3ad2ant3	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
8		eqid	|- ( quot1p ` R ) = ( quot1p ` R )
9		eqid	|- ( .r ` P ) = ( .r ` P )
10		eqid	|- ( -g ` P ) = ( -g ` P )
11	1 2 3 8 9 10	r1pval	|- ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
12	5 7 11	syl2anc	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
13	2	ply1ring	|- ( R e. Ring -> P e. Ring )
14	13	3ad2ant1	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Ring )
15		ringgrp	|- ( P e. Ring -> P e. Grp )
16	14 15	syl	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Grp )
17	8 2 3 4	q1pcl	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F ( quot1p ` R ) G ) e. B )
18	3 9	ringcl	|- ( ( P e. Ring /\ ( F ( quot1p ` R ) G ) e. B /\ G e. B ) -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
19	14 17 7 18	syl3anc	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
20	3 10	grpsubcl	|- ( ( P e. Grp /\ F e. B /\ ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B ) -> ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) e. B )
21	16 5 19 20	syl3anc	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) e. B )
22	12 21	eqeltrd	|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) e. B )