ply1vscl

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

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

Metamath Proof Explorer