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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐶 · 𝐵 ) ) 𝐸 𝐵 ) = ( 𝐴 𝐸 𝐵 ) )