Metamath Proof Explorer


Theorem ply1sca2

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

Ref Expression
Hypothesis ply1lmod.p P=Poly1R
Assertion ply1sca2 IR=ScalarP

Proof

Step Hyp Ref Expression
1 ply1lmod.p P=Poly1R
2 fvi RVIR=R
3 1 ply1sca RVR=ScalarP
4 2 3 eqtrd RVIR=ScalarP
5 fvprc ¬RVIR=
6 fvprc ¬RVPoly1R=
7 6 fveq2d ¬RVScalarPoly1R=Scalar
8 1 fveq2i ScalarP=ScalarPoly1R
9 scaid Scalar=SlotScalarndx
10 9 str0 =Scalar
11 7 8 10 3eqtr4g ¬RVScalarP=
12 5 11 eqtr4d ¬RVIR=ScalarP
13 4 12 pm2.61i IR=ScalarP