Metamath Proof Explorer

Theorem ply1sca

Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)

Ref Expression
Hypothesis ply1lmod.p 
|- P = ( Poly1 ` R )
Assertion ply1sca 
|- ( R e. V -> R = ( Scalar ` P ) )

Proof

Step Hyp Ref Expression
1 ply1lmod.p 
 |-  P = ( Poly1 ` R )
2 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
3 2 psr1sca 
 |-  ( R e. V -> R = ( Scalar ` ( PwSer1 ` R ) ) )
4 fvex 
 |-  ( Base ` ( 1o mPoly R ) ) e. _V
5 1 2 ply1val 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
6 eqid 
 |-  ( Scalar ` ( PwSer1 ` R ) ) = ( Scalar ` ( PwSer1 ` R ) )
7 5 6 resssca 
 |-  ( ( Base ` ( 1o mPoly R ) ) e. _V -> ( Scalar ` ( PwSer1 ` R ) ) = ( Scalar ` P ) )
8 4 7 ax-mp 
 |-  ( Scalar ` ( PwSer1 ` R ) ) = ( Scalar ` P )
9 3 8 eqtrdi 
 |-  ( R e. V -> R = ( Scalar ` P ) )