# 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 𝑌 = ( Poly1𝑅 )
ply1plusg.s 𝑆 = ( 1o mPoly 𝑅 )
ply1mulr.n · = ( .r𝑌 )
Assertion ply1mulr · = ( .r𝑆 )

### Proof

Step Hyp Ref Expression
1 ply1plusg.y 𝑌 = ( Poly1𝑅 )
2 ply1plusg.s 𝑆 = ( 1o mPoly 𝑅 )
3 ply1mulr.n · = ( .r𝑌 )
4 eqid ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
5 eqid ( .r𝑆 ) = ( .r𝑆 )
6 2 4 5 mplmulr ( .r𝑆 ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
7 eqid ( PwSer1𝑅 ) = ( PwSer1𝑅 )
8 eqid ( .r ‘ ( PwSer1𝑅 ) ) = ( .r ‘ ( PwSer1𝑅 ) )
9 7 4 8 psr1mulr ( .r ‘ ( PwSer1𝑅 ) ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
10 fvex ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V
11 1 7 ply1val 𝑌 = ( ( PwSer1𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
12 11 8 ressmulr ( ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ V → ( .r ‘ ( PwSer1𝑅 ) ) = ( .r𝑌 ) )
13 10 12 ax-mp ( .r ‘ ( PwSer1𝑅 ) ) = ( .r𝑌 )
14 6 9 13 3eqtr2i ( .r𝑆 ) = ( .r𝑌 )
15 3 14 eqtr4i · = ( .r𝑆 )