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 
|- P = ( Poly1 ` R )
r1padd1.u 
|- U = ( Base ` P )
r1padd1.n 
|- N = ( Unic1p ` R )
r1padd1.e 
|- E = ( rem1p ` R )
r1pcyc.p 
|- .+ = ( +g ` P )
r1pcyc.m 
|- .x. = ( .r ` P )
r1pcyc.r 
|- ( ph -> R e. Ring )
r1pcyc.a 
|- ( ph -> A e. U )
r1pcyc.b 
|- ( ph -> B e. N )
r1pcyc.c 
|- ( ph -> C e. U )
Assertion r1pcyc 
|- ( ph -> ( ( A .+ ( C .x. B ) ) E B ) = ( A E B ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p 
 |-  P = ( Poly1 ` R )
2 r1padd1.u 
 |-  U = ( Base ` P )
3 r1padd1.n 
 |-  N = ( Unic1p ` R )
4 r1padd1.e 
 |-  E = ( rem1p ` R )
5 r1pcyc.p 
 |-  .+ = ( +g ` P )
6 r1pcyc.m 
 |-  .x. = ( .r ` P )
7 r1pcyc.r 
 |-  ( ph -> R e. Ring )
8 r1pcyc.a 
 |-  ( ph -> A e. U )
9 r1pcyc.b 
 |-  ( ph -> B e. N )
10 r1pcyc.c 
 |-  ( ph -> C e. U )
11 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 7 11 syl 
 |-  ( ph -> P e. Ring )
13 12 ringgrpd 
 |-  ( ph -> P e. Grp )
14 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
15 14 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ B e. N ) -> ( A ( quot1p ` R ) B ) e. U )
16 7 8 9 15 syl3anc 
 |-  ( ph -> ( A ( quot1p ` R ) B ) e. U )
17 1 2 3 uc1pcl 
 |-  ( B e. N -> B e. U )
18 9 17 syl 
 |-  ( ph -> B e. U )
19 2 6 12 16 18 ringcld 
 |-  ( ph -> ( ( A ( quot1p ` R ) B ) .x. B ) e. U )
20 2 6 12 10 18 ringcld 
 |-  ( ph -> ( C .x. B ) e. U )
21 eqid 
 |-  ( -g ` P ) = ( -g ` P )
22 2 5 21 grppnpcan2 
 |-  ( ( P e. Grp /\ ( A e. U /\ ( ( A ( quot1p ` R ) B ) .x. B ) e. U /\ ( C .x. B ) e. U ) ) -> ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) B ) .x. B ) ) )
23 13 8 19 20 22 syl13anc 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) B ) .x. B ) ) )
24 2 5 13 8 20 grpcld 
 |-  ( ph -> ( A .+ ( C .x. B ) ) e. U )
25 4 1 2 14 6 21 r1pval 
 |-  ( ( ( A .+ ( C .x. B ) ) e. U /\ B e. U ) -> ( ( A .+ ( C .x. B ) ) E B ) = ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) .x. B ) ) )
26 24 18 25 syl2anc 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) E B ) = ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) .x. B ) ) )
27 14 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ ( C .x. B ) e. U /\ B e. N ) -> ( ( C .x. B ) ( quot1p ` R ) B ) e. U )
28 7 20 9 27 syl3anc 
 |-  ( ph -> ( ( C .x. B ) ( quot1p ` R ) B ) e. U )
29 2 5 6 ringdir 
 |-  ( ( P e. Ring /\ ( ( A ( quot1p ` R ) B ) e. U /\ ( ( C .x. B ) ( quot1p ` R ) B ) e. U /\ B e. U ) ) -> ( ( ( A ( quot1p ` R ) B ) .+ ( ( C .x. B ) ( quot1p ` R ) B ) ) .x. B ) = ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) ) )
30 12 16 28 18 29 syl13anc 
 |-  ( ph -> ( ( ( A ( quot1p ` R ) B ) .+ ( ( C .x. B ) ( quot1p ` R ) B ) ) .x. B ) = ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) ) )
31 1 2 3 14 7 8 9 20 5 q1pdir 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) = ( ( A ( quot1p ` R ) B ) .+ ( ( C .x. B ) ( quot1p ` R ) B ) ) )
32 31 oveq1d 
 |-  ( ph -> ( ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) .x. B ) = ( ( ( A ( quot1p ` R ) B ) .+ ( ( C .x. B ) ( quot1p ` R ) B ) ) .x. B ) )
33 eqid 
 |-  ( ||r ` P ) = ( ||r ` P )
34 2 33 6 dvdsrmul 
 |-  ( ( B e. U /\ C e. U ) -> B ( ||r ` P ) ( C .x. B ) )
35 18 10 34 syl2anc 
 |-  ( ph -> B ( ||r ` P ) ( C .x. B ) )
36 1 33 2 3 6 14 dvdsq1p 
 |-  ( ( R e. Ring /\ ( C .x. B ) e. U /\ B e. N ) -> ( B ( ||r ` P ) ( C .x. B ) <-> ( C .x. B ) = ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) ) )
37 7 20 9 36 syl3anc 
 |-  ( ph -> ( B ( ||r ` P ) ( C .x. B ) <-> ( C .x. B ) = ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) ) )
38 35 37 mpbid 
 |-  ( ph -> ( C .x. B ) = ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) )
39 38 oveq2d 
 |-  ( ph -> ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) = ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( ( ( C .x. B ) ( quot1p ` R ) B ) .x. B ) ) )
40 30 32 39 3eqtr4d 
 |-  ( ph -> ( ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) .x. B ) = ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) )
41 40 oveq2d 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A .+ ( C .x. B ) ) ( quot1p ` R ) B ) .x. B ) ) = ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) ) )
42 26 41 eqtrd 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) E B ) = ( ( A .+ ( C .x. B ) ) ( -g ` P ) ( ( ( A ( quot1p ` R ) B ) .x. B ) .+ ( C .x. B ) ) ) )
43 4 1 2 14 6 21 r1pval 
 |-  ( ( A e. U /\ B e. U ) -> ( A E B ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) B ) .x. B ) ) )
44 8 18 43 syl2anc 
 |-  ( ph -> ( A E B ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) B ) .x. B ) ) )
45 23 42 44 3eqtr4d 
 |-  ( ph -> ( ( A .+ ( C .x. B ) ) E B ) = ( A E B ) )