Metamath Proof Explorer


Theorem ply1ascl

Description: The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by Fan Zheng, 26-Jun-2016)

Ref Expression
Hypotheses ply1ascl.p P=Poly1R
ply1ascl.a A=algScP
Assertion ply1ascl A=algSc1𝑜mPolyR

Proof

Step Hyp Ref Expression
1 ply1ascl.p P=Poly1R
2 ply1ascl.a A=algScP
3 eqid ScalarP=ScalarP
4 eqid Scalar1𝑜mPolyR=Scalar1𝑜mPolyR
5 1 ply1sca RVR=ScalarP
6 5 fveq2d RVBaseR=BaseScalarP
7 eqid 1𝑜mPolyR=1𝑜mPolyR
8 1on 1𝑜On
9 8 a1i RV1𝑜On
10 id RVRV
11 7 9 10 mplsca RVR=Scalar1𝑜mPolyR
12 11 fveq2d RVBaseR=BaseScalar1𝑜mPolyR
13 eqid P=P
14 1 7 13 ply1vsca P=1𝑜mPolyR
15 14 a1i RVP=1𝑜mPolyR
16 15 oveqdr RVxBaseRyVxPy=x1𝑜mPolyRy
17 eqid 1P=1P
18 7 1 17 ply1mpl1 1P=11𝑜mPolyR
19 18 a1i RV1P=11𝑜mPolyR
20 fvexd RV1PV
21 3 4 6 12 16 19 20 asclpropd RValgScP=algSc1𝑜mPolyR
22 fvprc ¬RVPoly1R=
23 1 22 eqtrid ¬RVP=
24 reldmmpl ReldommPoly
25 24 ovprc2 ¬RV1𝑜mPolyR=
26 23 25 eqtr4d ¬RVP=1𝑜mPolyR
27 26 fveq2d ¬RValgScP=algSc1𝑜mPolyR
28 21 27 pm2.61i algScP=algSc1𝑜mPolyR
29 2 28 eqtri A=algSc1𝑜mPolyR