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

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

Proof

Step Hyp Ref Expression
1 r1pid2.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1pid2.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1pid2.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 r1pid2.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5 r1pid2.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
6 r1pid2.r ⊢ ( 𝜑 → 𝑅 ∈ Domn )
7 r1pid2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
8 r1pid2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
9 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
10 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
11 domnring ⊢ ( 𝑅 ∈ Domn → 𝑅 ∈ Ring )
12 6 11 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
13 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
14 13 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
15 12 7 8 14 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
16 1 2 3 uc1pcl ⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ∈ 𝑈 )
17 8 16 syl ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
18 1 9 3 uc1pn0 ⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
19 8 18 syl ⊢ ( 𝜑 → 𝐵 ≠ ( 0g ‘ 𝑃 ) )
20 17 19 eldifsnd ⊢ ( 𝜑 → 𝐵 ∈ ( 𝑈 ∖ { ( 0g ‘ 𝑃 ) } ) )
21 1 ply1domn ⊢ ( 𝑅 ∈ Domn → 𝑃 ∈ Domn )
22 6 21 syl ⊢ ( 𝜑 → 𝑃 ∈ Domn )
23 2 9 10 15 20 22 domneq0r ⊢ ( 𝜑 → ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
24 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
25 1 2 3 13 4 10 24 r1pid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
26 12 7 8 25 syl3anc ⊢ ( 𝜑 → 𝐴 = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
27 26 eqeq2d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ) )
28 eqcom ⊢ ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ↔ ( 𝐴 𝐸 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) )
29 27 28 bitr4di ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
30 domnring ⊢ ( 𝑃 ∈ Domn → 𝑃 ∈ Ring )
31 22 30 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
32 31 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
33 4 1 2 3 r1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
34 12 7 8 33 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 )
35 2 24 9 32 34 grplidd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) )
36 35 eqeq2d ⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( 𝐴 𝐸 𝐵 ) ) )
37 2 10 31 15 17 ringcld ⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 )
38 2 9 ring0cl ⊢ ( 𝑃 ∈ Ring → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
39 31 38 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑈 )
40 2 24 grprcan ⊢ ( ( 𝑃 ∈ Grp ∧ ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ∈ 𝑈 ∧ ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐴 𝐸 𝐵 ) ∈ 𝑈 ) ) → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
41 32 37 39 34 40 syl13anc ⊢ ( 𝜑 → ( ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) = ( ( 0g ‘ 𝑃 ) ( +g ‘ 𝑃 ) ( 𝐴 𝐸 𝐵 ) ) ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
42 29 36 41 3bitr2d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
43 2 10 9 31 17 ringlzd ⊢ ( 𝜑 → ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) = ( 0g ‘ 𝑃 ) )
44 43 oveq2d ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) = ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) )
45 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
46 2 9 45 grpsubid1 ⊢ ( ( 𝑃 ∈ Grp ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
47 32 7 46 syl2anc ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( 0g ‘ 𝑃 ) ) = 𝐴 )
48 44 47 eqtr2d ⊢ ( 𝜑 → 𝐴 = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) )
49 48 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) )
50 49 breq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) )
51 39 biantrurd ⊢ ( 𝜑 → ( ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ↔ ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ) )
52 13 1 2 5 45 10 3 q1peqb ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
53 12 7 8 52 syl3anc ⊢ ( 𝜑 → ( ( ( 0g ‘ 𝑃 ) ∈ 𝑈 ∧ ( 𝐷 ‘ ( 𝐴 ( -g ‘ 𝑃 ) ( ( 0g ‘ 𝑃 ) ( .r ‘ 𝑃 ) 𝐵 ) ) ) < ( 𝐷 ‘ 𝐵 ) ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
54 50 51 53 3bitrd ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ↔ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) = ( 0g ‘ 𝑃 ) ) )
55 23 42 54 3bitr4d ⊢ ( 𝜑 → ( ( 𝐴 𝐸 𝐵 ) = 𝐴 ↔ ( 𝐷 ‘ 𝐴 ) < ( 𝐷 ‘ 𝐵 ) ) )