Metamath Proof Explorer


Theorem ply1mulr

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

Ref Expression
Hypotheses ply1plusg.y Y = Poly 1 R
ply1plusg.s S = 1 𝑜 mPoly R
ply1mulr.n · ˙ = Y
Assertion ply1mulr · ˙ = S

Proof

Step Hyp Ref Expression
1 ply1plusg.y Y = Poly 1 R
2 ply1plusg.s S = 1 𝑜 mPoly R
3 ply1mulr.n · ˙ = Y
4 eqid 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
5 eqid S = S
6 2 4 5 mplmulr S = 1 𝑜 mPwSer R
7 eqid PwSer 1 R = PwSer 1 R
8 eqid PwSer 1 R = PwSer 1 R
9 7 4 8 psr1mulr PwSer 1 R = 1 𝑜 mPwSer R
10 fvex Base 1 𝑜 mPoly R V
11 1 7 ply1val Y = PwSer 1 R 𝑠 Base 1 𝑜 mPoly R
12 11 8 ressmulr Base 1 𝑜 mPoly R V PwSer 1 R = Y
13 10 12 ax-mp PwSer 1 R = Y
14 6 9 13 3eqtr2i S = Y
15 3 14 eqtr4i · ˙ = S