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 = Poly 1 R
Assertion ply1sca R V R = Scalar P

Proof

Step Hyp Ref Expression
1 ply1lmod.p P = Poly 1 R
2 eqid PwSer 1 R = PwSer 1 R
3 2 psr1sca R V R = Scalar PwSer 1 R
4 fvex Base 1 𝑜 mPoly R V
5 1 2 ply1val P = PwSer 1 R 𝑠 Base 1 𝑜 mPoly R
6 eqid Scalar PwSer 1 R = Scalar PwSer 1 R
7 5 6 resssca Base 1 𝑜 mPoly R V Scalar PwSer 1 R = Scalar P
8 4 7 ax-mp Scalar PwSer 1 R = Scalar P
9 3 8 eqtrdi R V R = Scalar P