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={\mathrm{Poly}}_1\left(R\right)$$
	r1padd1.u	$$⊢U={\mathrm{Base}}_P$$
	r1padd1.n	$$⊢N={Unic}_{\mathrm{1p}}\left(R\right)$$
	r1padd1.e	$$⊢E={rem}_{\mathrm{1p}}\left(R\right)$$
	r1padd1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	r1padd1.a	$$⊢\phi \to A\in U$$
	r1padd1.d	$$⊢\phi \to D\in N$$
	r1padd1.1	$$⊢\phi \to AED=BED$$
	r1padd1.2	$$⊢\underset{\dot{}}{+}={+}_P$$
	r1padd1.b	$$⊢\phi \to B\in U$$
	r1padd1.c	$$⊢\phi \to C\in U$$
Assertion	r1padd1	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right)ED=\left(B\underset{\dot{}}{+}C\right)ED$$

Proof

Step	Hyp	Ref	Expression
1		r1padd1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		r1padd1.u	$$⊢U={\mathrm{Base}}_P$$
3		r1padd1.n	$$⊢N={Unic}_{\mathrm{1p}}\left(R\right)$$
4		r1padd1.e	$$⊢E={rem}_{\mathrm{1p}}\left(R\right)$$
5		r1padd1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		r1padd1.a	$$⊢\phi \to A\in U$$
7		r1padd1.d	$$⊢\phi \to D\in N$$
8		r1padd1.1	$$⊢\phi \to AED=BED$$
9		r1padd1.2	$$⊢\underset{\dot{}}{+}={+}_P$$
10		r1padd1.b	$$⊢\phi \to B\in U$$
11		r1padd1.c	$$⊢\phi \to C\in U$$
12	1 2 3	uc1pcl	$$⊢D\in N\to D\in U$$
13	7 12	syl	$$⊢\phi \to D\in U$$
14		eqid	$$⊢{quot}_{\mathrm{1p}}\left(R\right)={quot}_{\mathrm{1p}}\left(R\right)$$
15		eqid	$$⊢{\cdot }_P={\cdot }_P$$
16		eqid	$$⊢{-}_P={-}_P$$
17	4 1 2 14 15 16	r1pval	$$⊢\left(A\in U\wedge D\in U\right)\to AED=A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
18	6 13 17	syl2anc	$$⊢\phi \to AED=A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
19	4 1 2 14 15 16	r1pval	$$⊢\left(B\in U\wedge D\in U\right)\to BED=B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
20	10 13 19	syl2anc	$$⊢\phi \to BED=B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
21	8 18 20	3eqtr3d	$$⊢\phi \to A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
22	21	oveq1d	$$⊢\phi \to \left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C=\left(B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
23		eqid	$$⊢{inv}_g\left(P\right)={inv}_g\left(P\right)$$
24	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
25	5 24	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
26	14 1 2 3	q1pcl	$$⊢\left(R\in \mathrm{Ring}\wedge A\in U\wedge D\in N\right)\to A{quot}_{\mathrm{1p}}\left(R\right)D\in U$$
27	5 6 7 26	syl3anc	$$⊢\phi \to A{quot}_{\mathrm{1p}}\left(R\right)D\in U$$
28	2 15 23 25 27 13	ringmneg1	$$⊢\phi \to {inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D={inv}_g\left(P\right)\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
29	28	oveq2d	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
30	25	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
31	2 9 30 6 11	grpcld	$$⊢\phi \to A\underset{\dot{}}{+}C\in U$$
32	2 15 25 27 13	ringcld	$$⊢\phi \to \left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U$$
33	2 9 23 16	grpsubval	$$⊢\left(A\underset{\dot{}}{+}C\in U\wedge \left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U\right)\to \left(A\underset{\dot{}}{+}C\right){-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
34	31 32 33	syl2anc	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right){-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
35	25	ringabld	$$⊢\phi \to P\in \mathrm{Abel}$$
36	2 9 16	abladdsub	$$⊢\left(P\in \mathrm{Abel}\wedge \left(A\in U\wedge C\in U\wedge \left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U\right)\right)\to \left(A\underset{\dot{}}{+}C\right){-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
37	35 6 11 32 36	syl13anc	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right){-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
38	29 34 37	3eqtr2d	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
39	14 1 2 3	q1pcl	$$⊢\left(R\in \mathrm{Ring}\wedge B\in U\wedge D\in N\right)\to B{quot}_{\mathrm{1p}}\left(R\right)D\in U$$
40	5 10 7 39	syl3anc	$$⊢\phi \to B{quot}_{\mathrm{1p}}\left(R\right)D\in U$$
41	2 15 23 25 40 13	ringmneg1	$$⊢\phi \to {inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D={inv}_g\left(P\right)\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
42	41	oveq2d	$$⊢\phi \to \left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
43	2 9 30 10 11	grpcld	$$⊢\phi \to B\underset{\dot{}}{+}C\in U$$
44	2 15 25 40 13	ringcld	$$⊢\phi \to \left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U$$
45	2 9 23 16	grpsubval	$$⊢\left(B\underset{\dot{}}{+}C\in U\wedge \left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U\right)\to \left(B\underset{\dot{}}{+}C\right){-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
46	43 44 45	syl2anc	$$⊢\phi \to \left(B\underset{\dot{}}{+}C\right){-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}{inv}_g\left(P\right)\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
47	2 9 16	abladdsub	$$⊢\left(P\in \mathrm{Abel}\wedge \left(B\in U\wedge C\in U\wedge \left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U\right)\right)\to \left(B\underset{\dot{}}{+}C\right){-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
48	35 10 11 44 47	syl13anc	$$⊢\phi \to \left(B\underset{\dot{}}{+}C\right){-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
49	42 46 48	3eqtr2d	$$⊢\phi \to \left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B{-}_P\left(\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)\underset{\dot{}}{+}C$$
50	22 38 49	3eqtr4d	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
51	50	oveq1d	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)ED=\left(\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)ED$$
52	2 23 30 27	grpinvcld	$$⊢\phi \to {inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\in U$$
53	1 2 3 4 9 15 5 31 7 52	r1pcyc	$$⊢\phi \to \left(\left(A\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)ED=\left(A\underset{\dot{}}{+}C\right)ED$$
54	2 23 30 40	grpinvcld	$$⊢\phi \to {inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right)\in U$$
55	1 2 3 4 9 15 5 43 7 54	r1pcyc	$$⊢\phi \to \left(\left(B\underset{\dot{}}{+}C\right)\underset{\dot{}}{+}\left({inv}_g\left(P\right)\left(B{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)ED=\left(B\underset{\dot{}}{+}C\right)ED$$
56	51 53 55	3eqtr3d	$$⊢\phi \to \left(A\underset{\dot{}}{+}C\right)ED=\left(B\underset{\dot{}}{+}C\right)ED$$