Theorem r1pcyc

Description: The polynomial remainder operation is periodic. See modcyc . (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	r1padd1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	r1padd1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	r1padd1.n	⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
	r1padd1.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
	r1pcyc.p	⊢ + = ( +g ‘ 𝑃 )
	r1pcyc.m	⊢ · = ( .r ‘ 𝑃 )
	r1pcyc.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	r1pcyc.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	r1pcyc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
	r1pcyc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion	r1pcyc	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( 𝐴 𝐸 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		r1padd1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		r1padd1.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
3		r1padd1.n	⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4		r1padd1.e	⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5		r1pcyc.p	⊢ + = ( +g ‘ 𝑃 )
6		r1pcyc.m	⊢ · = ( .r ‘ 𝑃 )
7		r1pcyc.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
8		r1pcyc.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
9		r1pcyc.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑁 )
10		r1pcyc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
11	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12	7 11	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
13	12	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
14		eqid	⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
15	14 1 2 3	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
16	7 8 9 15	syl3anc	⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
17	1 2 3	uc1pcl	⊢ ( 𝐵 ∈ 𝑁 → 𝐵 ∈ 𝑈 )
18	9 17	syl	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
19	2 6 12 16 18	ringcld	⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ∈ 𝑈 )
20	2 6 12 10 18	ringcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ 𝑈 )
21		eqid	⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
22	2 5 21	grppnpcan2	⊢ ( ( 𝑃 ∈ Grp ∧ ( 𝐴 ∈ 𝑈 ∧ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ∈ 𝑈 ∧ ( 𝐶 · 𝐵 ) ∈ 𝑈 ) ) → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
23	13 8 19 20 22	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
24	2 5 13 8 20	grpcld	⊢ ( 𝜑 → ( 𝐴 + ( 𝐶 · 𝐵 ) ) ∈ 𝑈 )
25	4 1 2 14 6 21	r1pval	⊢ ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
26	24 18 25	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
27	14 1 2 3	q1pcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 · 𝐵 ) ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
28	7 20 9 27	syl3anc	⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 )
29	2 5 6	ringdir	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ∧ ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ) → ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) + ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ) · 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
30	12 16 28 18 29	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) + ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ) · 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
31	1 2 3 14 7 8 9 20 5	q1pdir	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) = ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) + ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ) )
32	31	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) + ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) ) · 𝐵 ) )
33		eqid	⊢ ( ∥r ‘ 𝑃 ) = ( ∥r ‘ 𝑃 )
34	2 33 6	dvdsrmul	⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ) → 𝐵 ( ∥r ‘ 𝑃 ) ( 𝐶 · 𝐵 ) )
35	18 10 34	syl2anc	⊢ ( 𝜑 → 𝐵 ( ∥r ‘ 𝑃 ) ( 𝐶 · 𝐵 ) )
36	1 33 2 3 6 14	dvdsq1p	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐶 · 𝐵 ) ∈ 𝑈 ∧ 𝐵 ∈ 𝑁 ) → ( 𝐵 ( ∥r ‘ 𝑃 ) ( 𝐶 · 𝐵 ) ↔ ( 𝐶 · 𝐵 ) = ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
37	7 20 9 36	syl3anc	⊢ ( 𝜑 → ( 𝐵 ( ∥r ‘ 𝑃 ) ( 𝐶 · 𝐵 ) ↔ ( 𝐶 · 𝐵 ) = ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
38	35 37	mpbid	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) )
39	38	oveq2d	⊢ ( 𝜑 → ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( ( ( 𝐶 · 𝐵 ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
40	30 32 39	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) = ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) )
41	40	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) = ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) ) )
42	26 41	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) ( -g ‘ 𝑃 ) ( ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) + ( 𝐶 · 𝐵 ) ) ) )
43	4 1 2 14 6 21	r1pval	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
44	8 18 43	syl2anc	⊢ ( 𝜑 → ( 𝐴 𝐸 𝐵 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐵 ) · 𝐵 ) ) )
45	23 42 44	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( 𝐴 𝐸 𝐵 ) )