Theorem ply1vscl

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

	Ref	Expression
Hypotheses	ply1vscl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1vscl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1vscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ply1vscl.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1vscl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1vscl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	ply1vscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	ply1vscl	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ply1vscl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1vscl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		ply1vscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		ply1vscl.s	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		ply1vscl.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		ply1vscl.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
7		ply1vscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8	1 2	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
9		eqid	⊢ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) = ( Scalar ‘ ( 1o mPoly 𝑅 ) )
10		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
11	1 10 4	ply1vsca	⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
12		eqid	⊢ ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) ) = ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) )
13		1oex	⊢ 1o ∈ V
14	13	a1i	⊢ ( 𝜑 → 1o ∈ V )
15	10 14 5	mpllmodd	⊢ ( 𝜑 → ( 1o mPoly 𝑅 ) ∈ LMod )
16	10 14 5	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ ( 1o mPoly 𝑅 ) ) )
17	16	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) ) )
18	3 17	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) ) )
19	6 18	eleqtrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ ( 1o mPoly 𝑅 ) ) ) )
20	8 9 11 12 15 19 7	lmodvscld	⊢ ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ 𝐵 )