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 = Poly 1 R
coe1mul.t ˙ = Y
coe1mul.u · ˙ = R
coe1mul.b B = Base Y
Assertion coe1mul R Ring F B G B coe 1 F ˙ G = k 0 R x = 0 k coe 1 F x · ˙ coe 1 G k x

Proof

Step Hyp Ref Expression
1 coe1mul.s Y = Poly 1 R
2 coe1mul.t ˙ = Y
3 coe1mul.u · ˙ = R
4 coe1mul.b B = Base Y
5 id R Ring R Ring
6 1 4 ply1bascl F B F Base PwSer 1 R
7 1 4 ply1bascl G B G Base PwSer 1 R
8 eqid PwSer 1 R = PwSer 1 R
9 eqid 1 𝑜 mPoly R = 1 𝑜 mPoly R
10 eqid 1 𝑜 mPwSer R = 1 𝑜 mPwSer R
11 1 9 2 ply1mulr ˙ = 1 𝑜 mPoly R
12 9 10 11 mplmulr ˙ = 1 𝑜 mPwSer R
13 eqid PwSer 1 R = PwSer 1 R
14 8 10 13 psr1mulr PwSer 1 R = 1 𝑜 mPwSer R
15 12 14 eqtr4i ˙ = PwSer 1 R
16 eqid Base PwSer 1 R = Base PwSer 1 R
17 8 15 3 16 coe1mul2 R Ring F Base PwSer 1 R G Base PwSer 1 R coe 1 F ˙ G = k 0 R x = 0 k coe 1 F x · ˙ coe 1 G k x
18 5 6 7 17 syl3an R Ring F B G B coe 1 F ˙ G = k 0 R x = 0 k coe 1 F x · ˙ coe 1 G k x