Description: Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1val.1 | |
|
ply1val.2 | |
||
ply1bas.u | |
||
Assertion | ply1subrg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1val.1 | |
|
2 | ply1val.2 | |
|
3 | ply1bas.u | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 2 3 | ply1bas | |
7 | 1on | |
|
8 | 7 | a1i | |
9 | id | |
|
10 | 4 5 6 8 9 | mplsubrg | |
11 | eqidd | |
|
12 | 2 | psr1val | |
13 | 0ss | |
|
14 | 13 | a1i | |
15 | 4 12 14 | opsrbas | |
16 | 4 12 14 | opsrplusg | |
17 | 16 | oveqdr | |
18 | 4 12 14 | opsrmulr | |
19 | 18 | oveqdr | |
20 | 11 15 17 19 | subrgpropd | |
21 | 10 20 | eleqtrd | |