Metamath Proof Explorer


Theorem mplvsca

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mplvsca.p P = I mPoly R
mplvsca.n ˙ = P
mplvsca.k K = Base R
mplvsca.b B = Base P
mplvsca.m · ˙ = R
mplvsca.d D = h 0 I | h -1 Fin
mplvsca.x φ X K
mplvsca.f φ F B
Assertion mplvsca φ X ˙ F = D × X · ˙ f F

Proof

Step Hyp Ref Expression
1 mplvsca.p P = I mPoly R
2 mplvsca.n ˙ = P
3 mplvsca.k K = Base R
4 mplvsca.b B = Base P
5 mplvsca.m · ˙ = R
6 mplvsca.d D = h 0 I | h -1 Fin
7 mplvsca.x φ X K
8 mplvsca.f φ F B
9 eqid I mPwSer R = I mPwSer R
10 1 9 2 mplvsca2 ˙ = I mPwSer R
11 eqid Base I mPwSer R = Base I mPwSer R
12 1 9 4 11 mplbasss B Base I mPwSer R
13 12 8 sselid φ F Base I mPwSer R
14 9 10 3 11 5 6 7 13 psrvsca φ X ˙ F = D × X · ˙ f F