Description: Zero times a univariate polynomial is the zero polynomial ( lmod0vs analog.) (Contributed by AV, 2-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply10s0.p | |
|
ply10s0.b | |
||
ply10s0.m | |
||
ply10s0.e | |
||
Assertion | ply10s0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply10s0.p | |
|
2 | ply10s0.b | |
|
3 | ply10s0.m | |
|
4 | ply10s0.e | |
|
5 | 1 | ply1sca | |
6 | 5 | adantr | |
7 | 6 | fveq2d | |
8 | 4 7 | eqtrid | |
9 | 8 | oveq1d | |
10 | 1 | ply1lmod | |
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | 2 11 3 12 13 | lmod0vs | |
15 | 10 14 | sylan | |
16 | 9 15 | eqtrd | |