Metamath Proof Explorer

Theorem dvdsr1p

Description: Divisibility in a polynomial ring in terms of the remainder. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses dvdsq1p.p 
|- P = ( Poly1 ` R )
dvdsq1p.d 
|- .|| = ( ||r ` P )
dvdsq1p.b 
|- B = ( Base ` P )
dvdsq1p.c 
|- C = ( Unic1p ` R )
dvdsr1p.z 
|- .0. = ( 0g ` P )
dvdsr1p.e 
|- E = ( rem1p ` R )
Assertion dvdsr1p 
|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> ( F E G ) = .0. ) )

Proof

Step Hyp Ref Expression
1 dvdsq1p.p 
 |-  P = ( Poly1 ` R )
2 dvdsq1p.d 
 |-  .|| = ( ||r ` P )
3 dvdsq1p.b 
 |-  B = ( Base ` P )
4 dvdsq1p.c 
 |-  C = ( Unic1p ` R )
5 dvdsr1p.z 
 |-  .0. = ( 0g ` P )
6 dvdsr1p.e 
 |-  E = ( rem1p ` R )
7 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
8 7 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Ring )
9 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
10 8 9 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Grp )
11 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> F e. B )
12 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
13 12 1 3 4 q1pcl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F ( quot1p ` R ) G ) e. B )
14 1 3 4 uc1pcl 
 |-  ( G e. C -> G e. B )
15 14 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
16 eqid 
 |-  ( .r ` P ) = ( .r ` P )
17 3 16 ringcl 
 |-  ( ( P e. Ring /\ ( F ( quot1p ` R ) G ) e. B /\ G e. B ) -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
18 8 13 15 17 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
19 eqid 
 |-  ( -g ` P ) = ( -g ` P )
20 3 5 19 grpsubeq0 
 |-  ( ( 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 ) ) = .0. <-> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
21 10 11 18 20 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = .0. <-> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
22 6 1 3 12 16 19 r1pval 
 |-  ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
23 11 15 22 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) = ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
24 23 eqeq1d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F E G ) = .0. <-> ( F ( -g ` P ) ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = .0. ) )
25 1 2 3 4 16 12 dvdsq1p 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> F = ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) )
26 21 24 25 3bitr4rd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> ( F E G ) = .0. ) )