Description: The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | coe1mul.s | |
|
coe1mul.t | |
||
coe1mul.u | |
||
coe1mul.b | |
||
Assertion | coe1mul | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coe1mul.s | |
|
2 | coe1mul.t | |
|
3 | coe1mul.u | |
|
4 | coe1mul.b | |
|
5 | id | |
|
6 | 1 4 | ply1bascl | |
7 | 1 4 | ply1bascl | |
8 | eqid | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | 1 9 2 | ply1mulr | |
12 | 9 10 11 | mplmulr | |
13 | eqid | |
|
14 | 8 10 13 | psr1mulr | |
15 | 12 14 | eqtr4i | |
16 | eqid | |
|
17 | 8 15 3 16 | coe1mul2 | |
18 | 5 6 7 17 | syl3an | |