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)

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

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 r1padd1.e 
 |-  E = ( rem1p ` R )
5 r1pid2.r 
 |-  ( ph -> R e. IDomn )
6 r1pid2.d 
 |-  D = ( deg1 ` R )
7 r1pid2.p 
 |-  ( ph -> A e. U )
8 r1pid2.q 
 |-  ( ph -> B e. N )
9 5 idomringd 
 |-  ( ph -> R e. Ring )
10 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
11 eqid 
 |-  ( .r ` P ) = ( .r ` P )
12 eqid 
 |-  ( +g ` P ) = ( +g ` P )
13 1 2 3 10 4 11 12 r1pid 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> A = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) )
14 9 7 8 13 syl3anc 
 |-  ( ph -> A = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) )
15 14 eqeq2d 
 |-  ( ph -> ( ( A E B ) = A <-> ( A E B ) = ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) ) )
16 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 ) ) )
17 15 16 bitr4di 
 |-  ( ph -> ( ( A E B ) = A <-> ( ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) ( +g ` P ) ( A E B ) ) = ( A E B ) ) )
18 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
19 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
20 9 19 syl 
 |-  ( ph -> P e. Ring )
21 20 ringgrpd 
 |-  ( ph -> P e. Grp )
22 4 1 2 3 r1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( A E B ) e. U )
23 9 7 8 22 syl3anc 
 |-  ( ph -> ( A E B ) e. U )
24 2 12 18 21 23 grplidd 
 |-  ( ph -> ( ( 0g ` P ) ( +g ` P ) ( A E B ) ) = ( A E B ) )
25 24 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 ) ) )
26 10 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( A ( quot1p ` R ) B ) e. U )
27 9 7 8 26 syl3anc 
 |-  ( ph -> ( A ( quot1p ` R ) B ) e. U )
28 1 2 3 uc1pcl 
 |-  ( B e. N -> B e. U )
29 8 28 syl 
 |-  ( ph -> B e. U )
30 2 11 20 27 29 ringcld 
 |-  ( ph -> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) e. U )
31 2 18 ring0cl 
 |-  ( P e. Ring -> ( 0g ` P ) e. U )
32 9 19 31 3syl 
 |-  ( ph -> ( 0g ` P ) e. U )
33 2 12 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 ) ) )
34 21 30 32 23 33 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 ) ) )
35 17 25 34 3bitr2d 
 |-  ( ph -> ( ( A E B ) = A <-> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) ) )
36 isidom 
 |-  ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) )
37 5 36 sylib 
 |-  ( ph -> ( R e. CRing /\ R e. Domn ) )
38 37 simpld 
 |-  ( ph -> R e. CRing )
39 1 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
40 38 39 syl 
 |-  ( ph -> P e. CRing )
41 2 11 crngcom 
 |-  ( ( P e. CRing /\ B e. U /\ ( A ( quot1p ` R ) B ) e. U ) -> ( B ( .r ` P ) ( A ( quot1p ` R ) B ) ) = ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) )
42 40 29 27 41 syl3anc 
 |-  ( ph -> ( B ( .r ` P ) ( A ( quot1p ` R ) B ) ) = ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) )
43 42 eqeq1d 
 |-  ( ph -> ( ( B ( .r ` P ) ( A ( quot1p ` R ) B ) ) = ( 0g ` P ) <-> ( ( A ( quot1p ` R ) B ) ( .r ` P ) B ) = ( 0g ` P ) ) )
44 5 idomdomd 
 |-  ( ph -> R e. Domn )
45 1 ply1domn 
 |-  ( R e. Domn -> P e. Domn )
46 44 45 syl 
 |-  ( ph -> P e. Domn )
47 1 18 3 uc1pn0 
 |-  ( B e. N -> B =/= ( 0g ` P ) )
48 8 47 syl 
 |-  ( ph -> B =/= ( 0g ` P ) )
49 eqid 
 |-  ( RLReg ` P ) = ( RLReg ` P )
50 2 49 18 domnrrg 
 |-  ( ( P e. Domn /\ B e. U /\ B =/= ( 0g ` P ) ) -> B e. ( RLReg ` P ) )
51 46 29 48 50 syl3anc 
 |-  ( ph -> B e. ( RLReg ` P ) )
52 49 2 11 18 rrgeq0 
 |-  ( ( P e. Ring /\ B e. ( RLReg ` P ) /\ ( A ( quot1p ` R ) B ) e. U ) -> ( ( B ( .r ` P ) ( A ( quot1p ` R ) B ) ) = ( 0g ` P ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
53 20 51 27 52 syl3anc 
 |-  ( ph -> ( ( B ( .r ` P ) ( A ( quot1p ` R ) B ) ) = ( 0g ` P ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
54 35 43 53 3bitr2d 
 |-  ( ph -> ( ( A E B ) = A <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
55 2 11 18 20 29 ringlzd 
 |-  ( ph -> ( ( 0g ` P ) ( .r ` P ) B ) = ( 0g ` P ) )
56 55 oveq2d 
 |-  ( ph -> ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) = ( A ( -g ` P ) ( 0g ` P ) ) )
57 eqid 
 |-  ( -g ` P ) = ( -g ` P )
58 2 18 57 grpsubid1 
 |-  ( ( P e. Grp /\ A e. U ) -> ( A ( -g ` P ) ( 0g ` P ) ) = A )
59 21 7 58 syl2anc 
 |-  ( ph -> ( A ( -g ` P ) ( 0g ` P ) ) = A )
60 56 59 eqtr2d 
 |-  ( ph -> A = ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) )
61 60 fveq2d 
 |-  ( ph -> ( D ` A ) = ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) )
62 61 breq1d 
 |-  ( ph -> ( ( D ` A ) < ( D ` B ) <-> ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) )
63 32 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 ) ) ) )
64 10 1 2 6 57 11 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 ) ) )
65 9 7 8 64 syl3anc 
 |-  ( ph -> ( ( ( 0g ` P ) e. U /\ ( D ` ( A ( -g ` P ) ( ( 0g ` P ) ( .r ` P ) B ) ) ) < ( D ` B ) ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
66 62 63 65 3bitrd 
 |-  ( ph -> ( ( D ` A ) < ( D ` B ) <-> ( A ( quot1p ` R ) B ) = ( 0g ` P ) ) )
67 54 66 bitr4d 
 |-  ( ph -> ( ( A E B ) = A <-> ( D ` A ) < ( D ` B ) ) )