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 = {Poly}_{1} (R)$
	r1pid2.u	$⊢ U = {Base}_{P}$
	r1pid2.n	$⊢ N = {Unic}_{1p} (R)$
	r1pid2.e	$⊢ E = {rem}_{1p} (R)$
	r1pid2.d	$⊢ D = \deg_{1} (R)$
	r1pid2.r	$⊢ φ \to R \in Domn$
	r1pid2.a	$⊢ φ \to A \in U$
	r1pid2.b	$⊢ φ \to B \in N$
Assertion	r1pid2	$⊢ φ \to (A E B = A \leftrightarrow D (A) < D (B))$

Proof

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

Metamath Proof Explorer

Theorem r1pid2

Proof