This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplvsca2

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

Ref Expression
Hypotheses mplvsca2.p ⊢ P = I mPoly R
mplvsca2.s ⊢ S = I mPwSer R
mplvsca2.n ⊢ · ˙ = ⋅ P
Assertion mplvsca2 ⊢ · ˙ = ⋅ S

Proof

Step Hyp Ref Expression
1 mplvsca2.p ⊢ P = I mPoly R
2 mplvsca2.s ⊢ S = I mPwSer R
3 mplvsca2.n ⊢ · ˙ = ⋅ P
4 fvex ⊢ Base P ∈ V
5 eqid ⊢ Base P = Base P
6 1 2 5 mplval2 ⊢ P = S ↾ 𝑠 Base P
7 eqid ⊢ ⋅ S = ⋅ S
8 6 7 ressvsca ⊢ Base P ∈ V → ⋅ S = ⋅ P
9 4 8 ax-mp ⊢ ⋅ S = ⋅ P
10 3 9 eqtr4i ⊢ · ˙ = ⋅ S