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

Metamath Proof Explorer

Theorem r1padd1

Description: Addition property of the polynomial remainder operation, similar to modadd1 . (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 )
r1padd1.r 
|- ( ph -> R e. Ring )
r1padd1.a 
|- ( ph -> A e. U )
r1padd1.d 
|- ( ph -> D e. N )
r1padd1.1 
|- ( ph -> ( A E D ) = ( B E D ) )
r1padd1.2 
|- .+ = ( +g ` P )
r1padd1.b 
|- ( ph -> B e. U )
r1padd1.c 
|- ( ph -> C e. U )
Assertion r1padd1 
|- ( ph -> ( ( A .+ C ) E D ) = ( ( B .+ C ) E D ) )

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 r1padd1.r 
 |-  ( ph -> R e. Ring )
6 r1padd1.a 
 |-  ( ph -> A e. U )
7 r1padd1.d 
 |-  ( ph -> D e. N )
8 r1padd1.1 
 |-  ( ph -> ( A E D ) = ( B E D ) )
9 r1padd1.2 
 |-  .+ = ( +g ` P )
10 r1padd1.b 
 |-  ( ph -> B e. U )
11 r1padd1.c 
 |-  ( ph -> C e. U )
12 1 2 3 uc1pcl 
 |-  ( D e. N -> D e. U )
13 7 12 syl 
 |-  ( ph -> D e. U )
14 eqid 
 |-  ( quot1p ` R ) = ( quot1p ` R )
15 eqid 
 |-  ( .r ` P ) = ( .r ` P )
16 eqid 
 |-  ( -g ` P ) = ( -g ` P )
17 4 1 2 14 15 16 r1pval 
 |-  ( ( A e. U /\ D e. U ) -> ( A E D ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
18 6 13 17 syl2anc 
 |-  ( ph -> ( A E D ) = ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
19 4 1 2 14 15 16 r1pval 
 |-  ( ( B e. U /\ D e. U ) -> ( B E D ) = ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
20 10 13 19 syl2anc 
 |-  ( ph -> ( B E D ) = ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
21 8 18 20 3eqtr3d 
 |-  ( ph -> ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
22 21 oveq1d 
 |-  ( ph -> ( ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) = ( ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
23 eqid 
 |-  ( invg ` P ) = ( invg ` P )
24 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
25 5 24 syl 
 |-  ( ph -> P e. Ring )
26 14 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ A e. U /\ D e. N ) -> ( A ( quot1p ` R ) D ) e. U )
27 5 6 7 26 syl3anc 
 |-  ( ph -> ( A ( quot1p ` R ) D ) e. U )
28 2 15 23 25 27 13 ringmneg1 
 |-  ( ph -> ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) = ( ( invg ` P ) ` ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
29 28 oveq2d 
 |-  ( ph -> ( ( A .+ C ) .+ ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( A .+ C ) .+ ( ( invg ` P ) ` ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
30 25 ringgrpd 
 |-  ( ph -> P e. Grp )
31 2 9 30 6 11 grpcld 
 |-  ( ph -> ( A .+ C ) e. U )
32 2 15 25 27 13 ringcld 
 |-  ( ph -> ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) e. U )
33 2 9 23 16 grpsubval 
 |-  ( ( ( A .+ C ) e. U /\ ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) e. U ) -> ( ( A .+ C ) ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( A .+ C ) .+ ( ( invg ` P ) ` ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
34 31 32 33 syl2anc 
 |-  ( ph -> ( ( A .+ C ) ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( A .+ C ) .+ ( ( invg ` P ) ` ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
35 25 ringabld 
 |-  ( ph -> P e. Abel )
36 2 9 16 abladdsub 
 |-  ( ( P e. Abel /\ ( A e. U /\ C e. U /\ ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) e. U ) ) -> ( ( A .+ C ) ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
37 35 6 11 32 36 syl13anc 
 |-  ( ph -> ( ( A .+ C ) ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
38 29 34 37 3eqtr2d 
 |-  ( ph -> ( ( A .+ C ) .+ ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( A ( -g ` P ) ( ( A ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
39 14 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ B e. U /\ D e. N ) -> ( B ( quot1p ` R ) D ) e. U )
40 5 10 7 39 syl3anc 
 |-  ( ph -> ( B ( quot1p ` R ) D ) e. U )
41 2 15 23 25 40 13 ringmneg1 
 |-  ( ph -> ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) = ( ( invg ` P ) ` ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) )
42 41 oveq2d 
 |-  ( ph -> ( ( B .+ C ) .+ ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( B .+ C ) .+ ( ( invg ` P ) ` ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
43 2 9 30 10 11 grpcld 
 |-  ( ph -> ( B .+ C ) e. U )
44 2 15 25 40 13 ringcld 
 |-  ( ph -> ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) e. U )
45 2 9 23 16 grpsubval 
 |-  ( ( ( B .+ C ) e. U /\ ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) e. U ) -> ( ( B .+ C ) ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( B .+ C ) .+ ( ( invg ` P ) ` ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
46 43 44 45 syl2anc 
 |-  ( ph -> ( ( B .+ C ) ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( B .+ C ) .+ ( ( invg ` P ) ` ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) ) )
47 2 9 16 abladdsub 
 |-  ( ( P e. Abel /\ ( B e. U /\ C e. U /\ ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) e. U ) ) -> ( ( B .+ C ) ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
48 35 10 11 44 47 syl13anc 
 |-  ( ph -> ( ( B .+ C ) ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) = ( ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
49 42 46 48 3eqtr2d 
 |-  ( ph -> ( ( B .+ C ) .+ ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( B ( -g ` P ) ( ( B ( quot1p ` R ) D ) ( .r ` P ) D ) ) .+ C ) )
50 22 38 49 3eqtr4d 
 |-  ( ph -> ( ( A .+ C ) .+ ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) = ( ( B .+ C ) .+ ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) )
51 50 oveq1d 
 |-  ( ph -> ( ( ( A .+ C ) .+ ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) E D ) = ( ( ( B .+ C ) .+ ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) E D ) )
52 2 23 30 27 grpinvcld 
 |-  ( ph -> ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) e. U )
53 1 2 3 4 9 15 5 31 7 52 r1pcyc 
 |-  ( ph -> ( ( ( A .+ C ) .+ ( ( ( invg ` P ) ` ( A ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) E D ) = ( ( A .+ C ) E D ) )
54 2 23 30 40 grpinvcld 
 |-  ( ph -> ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) e. U )
55 1 2 3 4 9 15 5 43 7 54 r1pcyc 
 |-  ( ph -> ( ( ( B .+ C ) .+ ( ( ( invg ` P ) ` ( B ( quot1p ` R ) D ) ) ( .r ` P ) D ) ) E D ) = ( ( B .+ C ) E D ) )
56 51 53 55 3eqtr3d 
 |-  ( ph -> ( ( A .+ C ) E D ) = ( ( B .+ C ) E D ) )