Theorem r1p0

Description: Polynomial remainder operation of a division of the zero polynomial. (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)$$
	r1p0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	r1p0.d	$$⊢\phi \to D\in N$$
	r1p0.0	$$⊢\underset{\dot{}}{0}=0_P$$
Assertion	r1p0	$$⊢\phi \to \underset{\dot{}}{0}ED=\underset{\dot{}}{0}$$

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		r1p0.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		r1p0.d	$$⊢\phi \to D\in N$$
7		r1p0.0	$$⊢\underset{\dot{}}{0}=0_P$$
8	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
9	5 8	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
10	9	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(P\right)}$$
11	10	oveq1d	$$⊢\phi \to 0_R{\cdot }_P\underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\underset{\dot{}}{0}$$
12	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
13	5 12	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
14	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
15	2 7	ring0cl	$$⊢P\in \mathrm{Ring}\to \underset{\dot{}}{0}\in U$$
16	5 14 15	3syl	$$⊢\phi \to \underset{\dot{}}{0}\in U$$
17		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
18		eqid	$$⊢{\cdot }_P={\cdot }_P$$
19		eqid	$$⊢0_{\mathrm{Scalar}\left(P\right)}=0_{\mathrm{Scalar}\left(P\right)}$$
20	2 17 18 19 7	lmod0vs	$$⊢\left(P\in \mathrm{LMod}\wedge \underset{\dot{}}{0}\in U\right)\to 0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
21	13 16 20	syl2anc	$$⊢\phi \to 0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
22	11 21	eqtrd	$$⊢\phi \to 0_R{\cdot }_P\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
23	22	oveq1d	$$⊢\phi \to \left(0_R{\cdot }_P\underset{\dot{}}{0}\right)ED=\underset{\dot{}}{0}ED$$
24		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
25		eqid	$$⊢0_R=0_R$$
26	24 25	ring0cl	$$⊢R\in \mathrm{Ring}\to 0_R\in {\mathrm{Base}}_R$$
27	5 26	syl	$$⊢\phi \to 0_R\in {\mathrm{Base}}_R$$
28	1 2 3 4 5 16 6 18 24 27	r1pvsca	$$⊢\phi \to \left(0_R{\cdot }_P\underset{\dot{}}{0}\right)ED=0_R{\cdot }_P\left(\underset{\dot{}}{0}ED\right)$$
29	10	oveq1d	$$⊢\phi \to 0_R{\cdot }_P\left(\underset{\dot{}}{0}ED\right)=0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(\underset{\dot{}}{0}ED\right)$$
30	4 1 2 3	r1pcl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}\in U\wedge D\in N\right)\to \underset{\dot{}}{0}ED\in U$$
31	5 16 6 30	syl3anc	$$⊢\phi \to \underset{\dot{}}{0}ED\in U$$
32	2 17 18 19 7	lmod0vs	$$⊢\left(P\in \mathrm{LMod}\wedge \underset{\dot{}}{0}ED\in U\right)\to 0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(\underset{\dot{}}{0}ED\right)=\underset{\dot{}}{0}$$
33	13 31 32	syl2anc	$$⊢\phi \to 0_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(\underset{\dot{}}{0}ED\right)=\underset{\dot{}}{0}$$
34	28 29 33	3eqtrd	$$⊢\phi \to \left(0_R{\cdot }_P\underset{\dot{}}{0}\right)ED=\underset{\dot{}}{0}$$
35	23 34	eqtr3d	$$⊢\phi \to \underset{\dot{}}{0}ED=\underset{\dot{}}{0}$$