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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1pid2.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
r1pid2.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
r1pid2.p ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
r1pid2.q ⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
Assertion r1pid2 ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5 r1pid2.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
6 r1pid2.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
7 r1pid2.p ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
8 r1pid2.q ⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
9 5 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
11 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
12 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
13 1 2 3 10 4 11 12 r1pid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
14 9 7 8 13 syl3anc ⊢ ( 𝜑 → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
15 14 eqeq2d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ) )
16 eqcom ⊢ ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
17 15 16 bitr4di ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
18 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
19 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
20 9 19 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
21 20 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
22 4 1 2 3 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
23 9 7 8 22 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
24 2 12 18 21 23 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) )
25 24 eqeq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
26 10 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
27 9 7 8 26 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
28 1 2 3 uc1pcl ⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ∈ 𝑈 )
29 8 28 syl ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
30 2 11 20 27 29 ringcld ⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 )
31 2 18 ring0cl ⊢ ( 𝑃 ∈ Ring → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
32 9 19 31 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
33 2 12 grprcan ⊢ ( ( 𝑃 ∈ Grp ∧ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 ∧ ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 ) ) → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
34 21 30 32 23 33 syl13anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
35 17 25 34 3bitr2d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
36 isidom ⊢ ( 𝑅 ∈ IDomn ↔ ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
37 5 36 sylib ⊢ ( 𝜑 → ( 𝑅 ∈ CRing ∧ 𝑅 ∈ Domn ) )
38 37 simpld ⊢ ( 𝜑 → 𝑅 ∈ CRing )
39 1 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
40 38 39 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
41 2 11 crngcom ⊢ ( ( 𝑃 ∈ CRing ∧ 𝐵 ∈ 𝑈 ∧ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ) → ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) )
42 40 29 27 41 syl3anc ⊢ ( 𝜑 → ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) )
43 42 eqeq1d ⊢ ( 𝜑 → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
44 5 idomdomd ⊢ ( 𝜑 → 𝑅 ∈ Domn )
45 1 ply1domn ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
46 44 45 syl ⊢ ( 𝜑 → 𝑃 ∈ Domn )
47 1 18 3 uc1pn0 ⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
48 8 47 syl ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
49 eqid ⊢ ( RLReg ‘ 𝑃 ) = ( RLReg ‘ 𝑃 )
50 2 49 18 domnrrg ⊢ ( ( 𝑃 ∈ Domn ∧ 𝐵 ∈ 𝑈 ∧ 𝐵 ≠ ( 0g ‘ 𝑃 ) ) → 𝐵 ∈ ( RLReg ‘ 𝑃 ) )
51 46 29 48 50 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( RLReg ‘ 𝑃 ) )
52 49 2 11 18 rrgeq0 ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐵 ∈ ( RLReg ‘ 𝑃 ) ∧ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ) → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
53 20 51 27 52 syl3anc ⊢ ( 𝜑 → ( ( 𝐵 ( .r ‘ 𝑃 ) ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
54 35 43 53 3bitr2d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
55 2 11 18 20 29 ringlzd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) )
56 55 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) )
57 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
58 2 18 57 grpsubid1 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
59 21 7 58 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
60 56 59 eqtr2d ⊢ ( 𝜑 → 𝐴 = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) )
61 60 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) )
62 61 breq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) )
63 32 biantrurd ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ↔ ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ) )
64 10 1 2 6 57 11 3 q1peqb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
65 9 7 8 64 syl3anc ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
66 62 63 65 3bitrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
67 54 66 bitr4d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ) )