Metamath Proof Explorer


Theorem coe1mul

Description: The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul.s Y=Poly1R
coe1mul.t ˙=Y
coe1mul.u ·˙=R
coe1mul.b B=BaseY
Assertion coe1mul RRingFBGBcoe1F˙G=k0Rx=0kcoe1Fx·˙coe1Gkx

Proof

Step Hyp Ref Expression
1 coe1mul.s Y=Poly1R
2 coe1mul.t ˙=Y
3 coe1mul.u ·˙=R
4 coe1mul.b B=BaseY
5 id RRingRRing
6 1 4 ply1bascl FBFBasePwSer1R
7 1 4 ply1bascl GBGBasePwSer1R
8 eqid PwSer1R=PwSer1R
9 eqid 1𝑜mPolyR=1𝑜mPolyR
10 eqid 1𝑜mPwSerR=1𝑜mPwSerR
11 1 9 2 ply1mulr ˙=1𝑜mPolyR
12 9 10 11 mplmulr ˙=1𝑜mPwSerR
13 eqid PwSer1R=PwSer1R
14 8 10 13 psr1mulr PwSer1R=1𝑜mPwSerR
15 12 14 eqtr4i ˙=PwSer1R
16 eqid BasePwSer1R=BasePwSer1R
17 8 15 3 16 coe1mul2 RRingFBasePwSer1RGBasePwSer1Rcoe1F˙G=k0Rx=0kcoe1Fx·˙coe1Gkx
18 5 6 7 17 syl3an RRingFBGBcoe1F˙G=k0Rx=0kcoe1Fx·˙coe1Gkx