Theorem ply1vscl

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

	Ref	Expression
Hypotheses	ply1vscl.p	|- P = ( Poly1 ` R )
	ply1vscl.b	|- B = ( Base ` P )
	ply1vscl.k	|- K = ( Base ` R )
	ply1vscl.s	|- .x. = ( .s ` P )
	ply1vscl.r	|- ( ph -> R e. Ring )
	ply1vscl.c	|- ( ph -> C e. K )
	ply1vscl.x	|- ( ph -> X e. B )
Assertion	ply1vscl	|- ( ph -> ( C .x. X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		ply1vscl.p	|- P = ( Poly1 ` R )
2		ply1vscl.b	|- B = ( Base ` P )
3		ply1vscl.k	|- K = ( Base ` R )
4		ply1vscl.s	|- .x. = ( .s ` P )
5		ply1vscl.r	|- ( ph -> R e. Ring )
6		ply1vscl.c	|- ( ph -> C e. K )
7		ply1vscl.x	|- ( ph -> X e. B )
8	1 2	ply1bas	|- B = ( Base ` ( 1o mPoly R ) )
9		eqid	|- ( Scalar ` ( 1o mPoly R ) ) = ( Scalar ` ( 1o mPoly R ) )
10		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
11	1 10 4	ply1vsca	|- .x. = ( .s ` ( 1o mPoly R ) )
12		eqid	|- ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) = ( Base ` ( Scalar ` ( 1o mPoly R ) ) )
13		1oex	|- 1o e. _V
14	13	a1i	|- ( ph -> 1o e. _V )
15	10 14 5	mpllmodd	|- ( ph -> ( 1o mPoly R ) e. LMod )
16	10 14 5	mplsca	|- ( ph -> R = ( Scalar ` ( 1o mPoly R ) ) )
17	16	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) )
18	3 17	eqtrid	|- ( ph -> K = ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) )
19	6 18	eleqtrd	|- ( ph -> C e. ( Base ` ( Scalar ` ( 1o mPoly R ) ) ) )
20	8 9 11 12 15 19 7	lmodvscld	|- ( ph -> ( C .x. X ) e. B )