r1pcyc

Description: The polynomial remainder operation is periodic. See modcyc . (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)$
	r1pcyc.p	$⊢ \underset{˙}{+} = +_{P}$
	r1pcyc.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	r1pcyc.r	$⊢ φ \to R \in Ring$
	r1pcyc.a	$⊢ φ \to A \in U$
	r1pcyc.b	$⊢ φ \to B \in N$
	r1pcyc.c	$⊢ φ \to C \in U$
Assertion	r1pcyc	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) E B = A E 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		r1pcyc.p	$⊢ \underset{˙}{+} = +_{P}$
6		r1pcyc.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
7		r1pcyc.r	$⊢ φ \to R \in Ring$
8		r1pcyc.a	$⊢ φ \to A \in U$
9		r1pcyc.b	$⊢ φ \to B \in N$
10		r1pcyc.c	$⊢ φ \to C \in U$
11	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
12	7 11	syl	$⊢ φ \to P \in Ring$
13	12	ringgrpd	$⊢ φ \to P \in Grp$
14		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
15	14 1 2 3	q1pcl	$⊢ (R \in Ring \land A \in U \land B \in N) \to A {quot}_{1p} (R) B \in U$
16	7 8 9 15	syl3anc	$⊢ φ \to A {quot}_{1p} (R) B \in U$
17	1 2 3	uc1pcl	$⊢ B \in N \to B \in U$
18	9 17	syl	$⊢ φ \to B \in U$
19	2 6 12 16 18	ringcld	$⊢ φ \to (A {quot}_{1p} (R) B) \underset{˙}{\cdot} B \in U$
20	2 6 12 10 18	ringcld	$⊢ φ \to C \underset{˙}{\cdot} B \in U$
21		eqid	$⊢ -_{P} = -_{P}$
22	2 5 21	grppnpcan2	$⊢ (P \in Grp \land (A \in U \land (A {quot}_{1p} (R) B) \underset{˙}{\cdot} B \in U \land C \underset{˙}{\cdot} B \in U)) \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B)) = A -_{P} ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
23	13 8 19 20 22	syl13anc	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B)) = A -_{P} ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
24	2 5 13 8 20	grpcld	$⊢ φ \to A \underset{˙}{+} (C \underset{˙}{\cdot} B) \in U$
25	4 1 2 14 6 21	r1pval	$⊢ (A \underset{˙}{+} (C \underset{˙}{\cdot} B) \in U \land B \in U) \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) E B = (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
26	24 18 25	syl2anc	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) E B = (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
27	14 1 2 3	q1pcl	$⊢ (R \in Ring \land C \underset{˙}{\cdot} B \in U \land B \in N) \to (C \underset{˙}{\cdot} B) {quot}_{1p} (R) B \in U$
28	7 20 9 27	syl3anc	$⊢ φ \to (C \underset{˙}{\cdot} B) {quot}_{1p} (R) B \in U$
29	2 5 6	ringdir	$⊢ (P \in Ring \land (A {quot}_{1p} (R) B \in U \land (C \underset{˙}{\cdot} B) {quot}_{1p} (R) B \in U \land B \in U)) \to ((A {quot}_{1p} (R) B) \underset{˙}{+} ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B)) \underset{˙}{\cdot} B = ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
30	12 16 28 18 29	syl13anc	$⊢ φ \to ((A {quot}_{1p} (R) B) \underset{˙}{+} ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B)) \underset{˙}{\cdot} B = ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
31	1 2 3 14 7 8 9 20 5	q1pdir	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B = (A {quot}_{1p} (R) B) \underset{˙}{+} ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B)$
32	31	oveq1d	$⊢ φ \to ((A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B) \underset{˙}{\cdot} B = ((A {quot}_{1p} (R) B) \underset{˙}{+} ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B)) \underset{˙}{\cdot} B$
33		eqid	$⊢ ∥_{r} (P) = ∥_{r} (P)$
34	2 33 6	dvdsrmul	$⊢ (B \in U \land C \in U) \to B ∥_{r} (P) (C \underset{˙}{\cdot} B)$
35	18 10 34	syl2anc	$⊢ φ \to B ∥_{r} (P) (C \underset{˙}{\cdot} B)$
36	1 33 2 3 6 14	dvdsq1p	$⊢ (R \in Ring \land C \underset{˙}{\cdot} B \in U \land B \in N) \to (B ∥_{r} (P) (C \underset{˙}{\cdot} B) \leftrightarrow C \underset{˙}{\cdot} B = ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
37	7 20 9 36	syl3anc	$⊢ φ \to (B ∥_{r} (P) (C \underset{˙}{\cdot} B) \leftrightarrow C \underset{˙}{\cdot} B = ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
38	35 37	mpbid	$⊢ φ \to C \underset{˙}{\cdot} B = ((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B$
39	38	oveq2d	$⊢ φ \to ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B) = ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (((C \underset{˙}{\cdot} B) {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
40	30 32 39	3eqtr4d	$⊢ φ \to ((A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B) \underset{˙}{\cdot} B = ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B)$
41	40	oveq2d	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A \underset{˙}{+} (C \underset{˙}{\cdot} B)) {quot}_{1p} (R) B) \underset{˙}{\cdot} B) = (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B))$
42	26 41	eqtrd	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) E B = (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) -_{P} (((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B) \underset{˙}{+} (C \underset{˙}{\cdot} B))$
43	4 1 2 14 6 21	r1pval	$⊢ (A \in U \land B \in U) \to A E B = A -_{P} ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
44	8 18 43	syl2anc	$⊢ φ \to A E B = A -_{P} ((A {quot}_{1p} (R) B) \underset{˙}{\cdot} B)$
45	23 42 44	3eqtr4d	$⊢ φ \to (A \underset{˙}{+} (C \underset{˙}{\cdot} B)) E B = A E B$

Metamath Proof Explorer

Theorem r1pcyc

Proof