Metamath Proof Explorer


Theorem ply1subrg

Description: Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses ply1val.1 P=Poly1R
ply1val.2 S=PwSer1R
ply1bas.u U=BaseP
Assertion ply1subrg RRingUSubRingS

Proof

Step Hyp Ref Expression
1 ply1val.1 P=Poly1R
2 ply1val.2 S=PwSer1R
3 ply1bas.u U=BaseP
4 eqid 1𝑜mPwSerR=1𝑜mPwSerR
5 eqid 1𝑜mPolyR=1𝑜mPolyR
6 1 2 3 ply1bas U=Base1𝑜mPolyR
7 1on 1𝑜On
8 7 a1i RRing1𝑜On
9 id RRingRRing
10 4 5 6 8 9 mplsubrg RRingUSubRing1𝑜mPwSerR
11 eqidd RRingBase1𝑜mPwSerR=Base1𝑜mPwSerR
12 2 psr1val S=1𝑜ordPwSerR
13 0ss 1𝑜×1𝑜
14 13 a1i RRing1𝑜×1𝑜
15 4 12 14 opsrbas RRingBase1𝑜mPwSerR=BaseS
16 4 12 14 opsrplusg RRing+1𝑜mPwSerR=+S
17 16 oveqdr RRingxBase1𝑜mPwSerRyBase1𝑜mPwSerRx+1𝑜mPwSerRy=x+Sy
18 4 12 14 opsrmulr RRing1𝑜mPwSerR=S
19 18 oveqdr RRingxBase1𝑜mPwSerRyBase1𝑜mPwSerRx1𝑜mPwSerRy=xSy
20 11 15 17 19 subrgpropd RRingSubRing1𝑜mPwSerR=SubRingS
21 10 20 eleqtrd RRingUSubRingS