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

Proof

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

Metamath Proof Explorer

Theorem r1pid2

Proof