Metamath Proof Explorer

Theorem r1pid2

Description: Identity law for polynomial remainder operation: it leaves a polynomial A unchanged iff the degree of A is less than the degree of the divisor B . (Contributed by Thierry Arnoux, 2-Apr-2025) Generalize to domains. (Revised by SN, 21-Jun-2025)

Ref Expression
Hypotheses r1pid2.p 
|- P = ( Poly1 ` R )
r1pid2.u 
|- U = ( Base ` P )
r1pid2.n 
|- N = ( Unic1p ` R )
r1pid2.e 
|- E = ( rem1p ` R )
r1pid2.d 
|- D = ( deg1 ` R )
r1pid2.r 
|- ( ph -> R e. Domn )
r1pid2.a 
|- ( ph -> A e. U )
r1pid2.b 
|- ( ph -> B e. N )
Assertion r1pid2 
|- ( ph -> ( ( A E B ) = A <-> ( D ` A ) < ( D ` B ) ) )

Proof

Step Hyp Ref Expression
1 r1pid2.p 
 |-  P = ( Poly1 ` R )
2 r1pid2.u 
 |-  U = ( Base ` P )
3 r1pid2.n 
 |-  N = ( Unic1p ` R )
4 r1pid2.e 
 |-  E = ( rem1p ` R )
5 r1pid2.d 
 |-  D = ( deg1 ` R )
6 r1pid2.r 
 |-  ( ph -> R e. Domn )
7 r1pid2.a 
 |-  ( ph -> A e. U )
8 r1pid2.b 
 |-  ( ph -> B e. N )
9 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
10 eqid 
 |-  ( .r ` P ) = ( .r ` P )
11 domnring 
 |-  ( R e. Domn -> R e. Ring )
12 6 11 syl 
 |-  ( ph -> R e. Ring )
13 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
14 13 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( A ( quot1p ` R ) B ) e. U )
15 12 7 8 14 syl3anc 
 |-  ( ph -> ( A ( quot1p ` R ) B ) e. U )
16 1 2 3 uc1pcl 
 |-  ( B e. N -> B e. U )
17 8 16 syl 
 |-  ( ph -> B e. U )
18 1 9 3 uc1pn0 
 |-  ( B e. N -> B =/= ( 0g ` P ) )
19 8 18 syl 
 |-  ( ph -> B =/= ( 0g ` P ) )
20 17 19 eldifsnd 
 |-  ( ph -> B e. ( U \ { ( 0g ` P ) } ) )
21 1 ply1domn 
 |-  ( R e. Domn -> P e. Domn )
22 6 21 syl 
 |-  ( ph -> P e. Domn )
23 2 9 10 15 20 22 domneq0r 
 |-  ( ph -> ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
24 eqid 
 |-  ( +g ` P ) = ( +g ` P )
25 1 2 3 13 4 10 24 r1pid 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> A = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) )
26 12 7 8 25 syl3anc 
 |-  ( ph -> A = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) )
27 26 eqeq2d 
 |-  ( ph -> ( ( A E B ) = A <-> ( A E B ) = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) ) )
28 eqcom 
 |-  ( ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( A E B ) <-> ( A E B ) = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) )
29 27 28 bitr4di 
 |-  ( ph -> ( ( A E B ) = A <-> ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( A E B ) ) )
30 domnring 
 |-  ( P e. Domn -> P e. Ring )
31 22 30 syl 
 |-  ( ph -> P e. Ring )
32 31 ringgrpd 
 |-  ( ph -> P e. Grp )
33 4 1 2 3 r1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( A E B ) e. U )
34 12 7 8 33 syl3anc 
 |-  ( ph -> ( A E B ) e. U )
35 2 24 9 32 34 grplidd 
 |-  ( ph -> ( ( 0g ` P ) ( +g ` P ) ( A E B ) ) = ( A E B ) )
36 35 eqeq2d 
 |-  ( ph -> ( ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( ( 0g ` P ) ( +g ` P ) ( A E B ) ) <-> ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( A E B ) ) )
37 2 10 31 15 17 ringcld 
 |-  ( ph -> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) e. U )
38 2 9 ring0cl 
 |-  ( P e. Ring -> ( 0g ` P ) e. U )
39 31 38 syl 
 |-  ( ph -> ( 0g ` P ) e. U )
40 2 24 grprcan 
 |-  ( ( P e. Grp /\ ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) e. U /\ ( 0g ` P ) e. U /\ ( A E B ) e. U ) ) -> ( ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( ( 0g ` P ) ( +g ` P ) ( A E B ) ) <-> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) ) )
41 32 37 39 34 40 syl13anc 
 |-  ( ph -> ( ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( ( 0g ` P ) ( +g ` P ) ( A E B ) ) <-> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) ) )
42 29 36 41 3bitr2d 
 |-  ( ph -> ( ( A E B ) = A <-> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) ) )
43 2 10 9 31 17 ringlzd 
 |-  ( ph -> ( ( 0g ` P ) ( .r ` P ) B ) = ( 0g ` P ) )
44 43 oveq2d 
 |-  ( ph -> ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) = ( A ( -g ` P ) ( 0g ` P ) ) )
45 eqid 
 |-  ( -g ` P ) = ( -g ` P )
46 2 9 45 grpsubid1 
 |-  ( ( P e. Grp /\ A e. U ) -> ( A ( -g ` P ) ( 0g ` P ) ) = A )
47 32 7 46 syl2anc 
 |-  ( ph -> ( A ( -g ` P ) ( 0g ` P ) ) = A )
48 44 47 eqtr2d 
 |-  ( ph -> A = ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) )
49 48 fveq2d 
 |-  ( ph -> ( D ` A ) = ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) )
50 49 breq1d 
 |-  ( ph -> ( ( D ` A ) < ( D ` B ) <-> ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) )
51 39 biantrurd 
 |-  ( ph -> ( ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) <-> ( ( 0g ` P ) e. U /\ ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) ) )
52 13 1 2 5 45 10 3 q1peqb 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( ( ( 0g ` P ) e. U /\ ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
53 12 7 8 52 syl3anc 
 |-  ( ph -> ( ( ( 0g ` P ) e. U /\ ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
54 50 51 53 3bitrd 
 |-  ( ph -> ( ( D ` A ) < ( D ` B ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
55 23 42 54 3bitr4d 
 |-  ( ph -> ( ( A E B ) = A <-> ( D ` A ) < ( D ` B ) ) )