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

Metamath Proof Explorer

Theorem mplmulr

Description: Value of multiplication in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses mplplusg.y ⊢ Y = I mPoly R
mplplusg.s ⊢ S = I mPwSer R
mplmulr.n ⊢ · ˙ = ⋅ Y
Assertion mplmulr ⊢ · ˙ = ⋅ S

Proof

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