This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )