Theorem r1pvsca

Description: Scalar multiplication property of the polynomial remainder operation. (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)$$
	r1pvsca.6	$$⊢\phi \to R\in \mathrm{Ring}$$
	r1pvsca.7	$$⊢\phi \to A\in U$$
	r1pvsca.10	$$⊢\phi \to D\in N$$
	r1pvsca.1	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
	r1pvsca.k	$$⊢K={\mathrm{Base}}_R$$
	r1pvsca.2	$$⊢\phi \to B\in K$$
Assertion	r1pvsca	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right)ED=B\underset{\dot{}}{\times }\left(AED\right)$$

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		r1pvsca.6	$$⊢\phi \to R\in \mathrm{Ring}$$
6		r1pvsca.7	$$⊢\phi \to A\in U$$
7		r1pvsca.10	$$⊢\phi \to D\in N$$
8		r1pvsca.1	$$⊢\underset{\dot{}}{\times }={\cdot }_P$$
9		r1pvsca.k	$$⊢K={\mathrm{Base}}_R$$
10		r1pvsca.2	$$⊢\phi \to B\in K$$
11		eqid	$$⊢{quot}_{\mathrm{1p}}\left(R\right)={quot}_{\mathrm{1p}}\left(R\right)$$
12	11 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$$
13	5 6 7 12	syl3anc	$$⊢\phi \to A{quot}_{\mathrm{1p}}\left(R\right)D\in U$$
14	1 2 3	uc1pcl	$$⊢D\in N\to D\in U$$
15	7 14	syl	$$⊢\phi \to D\in U$$
16		eqid	$$⊢{\cdot }_P={\cdot }_P$$
17	1 16 2 9 8	ply1ass23l	$$⊢\left(R\in \mathrm{Ring}\wedge \left(B\in K\wedge A{quot}_{\mathrm{1p}}\left(R\right)D\in U\wedge D\in U\right)\right)\to \left(B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\right){\cdot }_{P}D=B\underset{\dot{}}{\times }\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
18	5 10 13 15 17	syl13anc	$$⊢\phi \to \left(B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\right){\cdot }_{P}D=B\underset{\dot{}}{\times }\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
19	18	oveq2d	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{\times }A\right){-}_P\left(B\underset{\dot{}}{\times }\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)$$
20	1 2 3 11 5 6 7 8 9 10	q1pvsca	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D=B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)$$
21	20	oveq1d	$$⊢\phi \to \left(\left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D=\left(B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\right){\cdot }_{P}D$$
22	21	oveq2d	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(\left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=\left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(B\underset{\dot{}}{\times }\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right)\right){\cdot }_{P}D\right)$$
23		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
24		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
25		eqid	$$⊢{-}_P={-}_P$$
26	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
27	5 26	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
28	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
29	5 28	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
30	29	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
31	9 30	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
32	10 31	eleqtrd	$$⊢\phi \to B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
33	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
34	5 33	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
35	2 16 34 13 15	ringcld	$$⊢\phi \to \left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\in U$$
36	2 8 23 24 25 27 32 6 35	lmodsubdi	$$⊢\phi \to B\underset{\dot{}}{\times }\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)=\left(B\underset{\dot{}}{\times }A\right){-}_P\left(B\underset{\dot{}}{\times }\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)$$
37	19 22 36	3eqtr4d	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(\left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)=B\underset{\dot{}}{\times }\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)$$
38	2 23 8 24 27 32 6	lmodvscld	$$⊢\phi \to B\underset{\dot{}}{\times }A\in U$$
39	4 1 2 11 16 25	r1pval	$$⊢\left(B\underset{\dot{}}{\times }A\in U\wedge D\in U\right)\to \left(B\underset{\dot{}}{\times }A\right)ED=\left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(\left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
40	38 15 39	syl2anc	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right)ED=\left(B\underset{\dot{}}{\times }A\right){-}_P\left(\left(\left(B\underset{\dot{}}{\times }A\right){quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
41	4 1 2 11 16 25	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)$$
42	6 15 41	syl2anc	$$⊢\phi \to AED=A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)$$
43	42	oveq2d	$$⊢\phi \to B\underset{\dot{}}{\times }\left(AED\right)=B\underset{\dot{}}{\times }\left(A{-}_P\left(\left(A{quot}_{\mathrm{1p}}\left(R\right)D\right){\cdot }_{P}D\right)\right)$$
44	37 40 43	3eqtr4d	$$⊢\phi \to \left(B\underset{\dot{}}{\times }A\right)ED=B\underset{\dot{}}{\times }\left(AED\right)$$