Description: Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | evl1addd.q | |
|
evl1addd.p | |
||
evl1addd.b | |
||
evl1addd.u | |
||
evl1addd.1 | |
||
evl1addd.2 | |
||
evl1addd.3 | |
||
evl1vsd.4 | |
||
evl1vsd.s | |
||
evl1vsd.t | |
||
Assertion | evl1vsd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | evl1addd.q | |
|
2 | evl1addd.p | |
|
3 | evl1addd.b | |
|
4 | evl1addd.u | |
|
5 | evl1addd.1 | |
|
6 | evl1addd.2 | |
|
7 | evl1addd.3 | |
|
8 | evl1vsd.4 | |
|
9 | evl1vsd.s | |
|
10 | evl1vsd.t | |
|
11 | eqid | |
|
12 | 1 2 3 11 4 5 8 6 | evl1scad | |
13 | eqid | |
|
14 | 1 2 3 4 5 6 12 7 13 10 | evl1muld | |
15 | 2 | ply1assa | |
16 | 5 15 | syl | |
17 | 2 | ply1sca | |
18 | 5 17 | syl | |
19 | 18 | fveq2d | |
20 | 3 19 | eqtrid | |
21 | 8 20 | eleqtrd | |
22 | 7 | simpld | |
23 | eqid | |
|
24 | eqid | |
|
25 | 11 23 24 4 13 9 | asclmul1 | |
26 | 16 21 22 25 | syl3anc | |
27 | 26 | eleq1d | |
28 | 26 | fveq2d | |
29 | 28 | fveq1d | |
30 | 29 | eqeq1d | |
31 | 27 30 | anbi12d | |
32 | 14 31 | mpbid | |