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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
r1padd1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
r1padd1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
r1padd1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
r1padd1.1 ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐷 ) = ( 𝐵 𝐸 𝐷 ) )
r1padd1.2 ⊢ + = ( +g ‘ 𝑃 )
r1padd1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
r1padd1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
Assertion r1padd1 ( 𝜑 → ( ( 𝐴 + 𝐶 ) 𝐸 𝐷 ) = ( ( 𝐵 + 𝐶 ) 𝐸 𝐷 ) )

Proof

Step Hyp Ref Expression
1 r1padd1.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 r1padd1.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
3 r1padd1.n ⊢ 𝑁 = ( Unic1p ‘ 𝑅 )
4 r1padd1.e ⊢ 𝐸 = ( rem1p ‘ 𝑅 )
5 r1padd1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 r1padd1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
7 r1padd1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑁 )
8 r1padd1.1 ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐷 ) = ( 𝐵 𝐸 𝐷 ) )
9 r1padd1.2 ⊢ + = ( +g ‘ 𝑃 )
10 r1padd1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
11 r1padd1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
12 1 2 3 uc1pcl ⊢ ( 𝐷 ∈ 𝑁 → 𝐷 ∈ 𝑈 )
13 7 12 syl ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
14 eqid ⊢ ( quot1p ‘ 𝑅 ) = ( quot1p ‘ 𝑅 )
15 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
16 eqid ⊢ ( -g ‘ 𝑃 ) = ( -g ‘ 𝑃 )
17 4 1 2 14 15 16 r1pval ⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) → ( 𝐴 𝐸 𝐷 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
18 6 13 17 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝐸 𝐷 ) = ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
19 4 1 2 14 15 16 r1pval ⊢ ( ( 𝐵 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) → ( 𝐵 𝐸 𝐷 ) = ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
20 10 13 19 syl2anc ⊢ ( 𝜑 → ( 𝐵 𝐸 𝐷 ) = ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
21 8 18 20 3eqtr3d ⊢ ( 𝜑 → ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
22 21 oveq1d ⊢ ( 𝜑 → ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) = ( ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
23 eqid ⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
24 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
25 5 24 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
26 14 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁 ) → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
27 5 6 7 26 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
28 2 15 23 25 27 13 ringmneg1 ⊢ ( 𝜑 → ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) = ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
29 28 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
30 25 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
31 2 9 30 6 11 grpcld ⊢ ( 𝜑 → ( 𝐴 + 𝐶 ) ∈ 𝑈 )
32 2 15 25 27 13 ringcld ⊢ ( 𝜑 → ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 )
33 2 9 23 16 grpsubval ⊢ ( ( ( 𝐴 + 𝐶 ) ∈ 𝑈 ∧ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 ) → ( ( 𝐴 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
34 31 32 33 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
35 25 ringabld ⊢ ( 𝜑 → 𝑃 ∈ Abel )
36 2 9 16 abladdsub ⊢ ( ( 𝑃 ∈ Abel ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ∧ ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 ) ) → ( ( 𝐴 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
37 35 6 11 32 36 syl13anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
38 29 34 37 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐴 ( -g ‘ 𝑃 ) ( ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
39 14 1 2 3 q1pcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐵 ∈ 𝑈 ∧ 𝐷 ∈ 𝑁 ) → ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
40 5 10 7 39 syl3anc ⊢ ( 𝜑 → ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ∈ 𝑈 )
41 2 15 23 25 40 13 ringmneg1 ⊢ ( 𝜑 → ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) = ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
42 41 oveq2d ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
43 2 9 30 10 11 grpcld ⊢ ( 𝜑 → ( 𝐵 + 𝐶 ) ∈ 𝑈 )
44 2 15 25 40 13 ringcld ⊢ ( 𝜑 → ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 )
45 2 9 23 16 grpsubval ⊢ ( ( ( 𝐵 + 𝐶 ) ∈ 𝑈 ∧ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 ) → ( ( 𝐵 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
46 43 44 45 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 + 𝐶 ) + ( ( invg ‘ 𝑃 ) ‘ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) ) )
47 2 9 16 abladdsub ⊢ ( ( 𝑃 ∈ Abel ∧ ( 𝐵 ∈ 𝑈 ∧ 𝐶 ∈ 𝑈 ∧ ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ∈ 𝑈 ) ) → ( ( 𝐵 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
48 35 10 11 44 47 syl13anc ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
49 42 46 48 3eqtr2d ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 ( -g ‘ 𝑃 ) ( ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ( .r ‘ 𝑃 ) 𝐷 ) ) + 𝐶 ) )
50 22 38 49 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) = ( ( 𝐵 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) )
51 50 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) 𝐸 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) 𝐸 𝐷 ) )
52 2 23 30 27 grpinvcld ⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ∈ 𝑈 )
53 1 2 3 4 9 15 5 31 7 52 r1pcyc ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐴 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) 𝐸 𝐷 ) = ( ( 𝐴 + 𝐶 ) 𝐸 𝐷 ) )
54 2 23 30 40 grpinvcld ⊢ ( 𝜑 → ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ∈ 𝑈 )
55 1 2 3 4 9 15 5 43 7 54 r1pcyc ⊢ ( 𝜑 → ( ( ( 𝐵 + 𝐶 ) + ( ( ( invg ‘ 𝑃 ) ‘ ( 𝐵 ( quot1p ‘ 𝑅 ) 𝐷 ) ) ( .r ‘ 𝑃 ) 𝐷 ) ) 𝐸 𝐷 ) = ( ( 𝐵 + 𝐶 ) 𝐸 𝐷 ) )
56 51 53 55 3eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐶 ) 𝐸 𝐷 ) = ( ( 𝐵 + 𝐶 ) 𝐸 𝐷 ) )