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 ) )