Metamath Proof Explorer


Theorem ply1vscl

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

Ref Expression
Hypotheses ply1vscl.p P = Poly 1 R
ply1vscl.b B = Base P
ply1vscl.k K = Base R
ply1vscl.s · ˙ = P
ply1vscl.r φ R Ring
ply1vscl.c φ C K
ply1vscl.x φ X B
Assertion ply1vscl φ C · ˙ X B

Proof

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 · ˙ = P
5 ply1vscl.r φ R Ring
6 ply1vscl.c φ C K
7 ply1vscl.x φ X 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 · ˙ = 1 𝑜 mPoly R
12 eqid Base Scalar 1 𝑜 mPoly R = Base Scalar 1 𝑜 mPoly R
13 1oex 1 𝑜 V
14 13 a1i φ 1 𝑜 V
15 10 14 5 mpllmodd φ 1 𝑜 mPoly R LMod
16 10 14 5 mplsca φ R = Scalar 1 𝑜 mPoly R
17 16 fveq2d φ Base R = Base Scalar 1 𝑜 mPoly R
18 3 17 eqtrid φ K = Base Scalar 1 𝑜 mPoly R
19 6 18 eleqtrd φ C Base Scalar 1 𝑜 mPoly R
20 8 9 11 12 15 19 7 lmodvscld φ C · ˙ X B