Theorem ply1vscl

Description: Closure of scalar multiplication for univariate polynomials. (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	ply1vscl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1vscl.b	$$⊢B={\mathrm{Base}}_P$$
	ply1vscl.k	$$⊢K={\mathrm{Base}}_R$$
	ply1vscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	ply1vscl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ply1vscl.c	$$⊢\phi \to C\in K$$
	ply1vscl.x	$$⊢\phi \to X\in B$$
Assertion	ply1vscl	$$⊢\phi \to C\underset{\dot{}}{·}X\in B$$

Proof

Step	Hyp	Ref	Expression
1		ply1vscl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1vscl.b	$$⊢B={\mathrm{Base}}_P$$
3		ply1vscl.k	$$⊢K={\mathrm{Base}}_R$$
4		ply1vscl.s	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
5		ply1vscl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		ply1vscl.c	$$⊢\phi \to C\in K$$
7		ply1vscl.x	$$⊢\phi \to X\in B$$
8	1 2	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		eqid	$$⊢\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)=\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
10		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
11	1 10 4	ply1vsca	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
13		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
14	13	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
15	10 14 5	mpllmodd	$$⊢\phi \to 1_{𝑜}\mathrm{mPoly}R\in \mathrm{LMod}$$
16	10 14 5	mplsca	$$⊢\phi \to R=\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
17	16	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	3 17	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	6 18	eleqtrd	$$⊢\phi \to C\in {\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20	8 9 11 12 15 19 7	lmodvscld	$$⊢\phi \to C\underset{\dot{}}{·}X\in B$$