Theorem ply10s0

Description: Zero times a univariate polynomial is the zero polynomial ( lmod0vs analog.) (Contributed by AV, 2-Dec-2019)

	Ref	Expression
Hypotheses	ply10s0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply10s0.b	$$⊢B={\mathrm{Base}}_P$$
	ply10s0.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
	ply10s0.e	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	ply10s0	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\ast }M=0_P$$

Proof

Step	Hyp	Ref	Expression
1		ply10s0.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply10s0.b	$$⊢B={\mathrm{Base}}_P$$
3		ply10s0.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
4		ply10s0.e	$$⊢\underset{\dot{}}{0}=0_R$$
5	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
6	5	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to R=\mathrm{Scalar}\left(P\right)$$
7	6	fveq2d	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to 0_R=0_{\mathrm{Scalar}\left(P\right)}$$
8	4 7	syl5eq	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \underset{\dot{}}{0}=0_{\mathrm{Scalar}\left(P\right)}$$
9	8	oveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\ast }M=0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{\ast }M$$
10	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
11		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
12		eqid	$$⊢0_{\mathrm{Scalar}\left(P\right)}=0_{\mathrm{Scalar}\left(P\right)}$$
13		eqid	$$⊢0_P=0_P$$
14	2 11 3 12 13	lmod0vs	$$⊢\left(P\in \mathrm{LMod}\wedge M\in B\right)\to 0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{\ast }M=0_P$$
15	10 14	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to 0_{\mathrm{Scalar}\left(P\right)}\underset{\dot{}}{\ast }M=0_P$$
16	9 15	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge M\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\ast }M=0_P$$