Description: The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by Fan Zheng, 26-Jun-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1ascl.p | |
|
ply1ascl.a | |
||
Assertion | ply1ascl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1ascl.p | |
|
2 | ply1ascl.a | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | 1 | ply1sca | |
6 | 5 | fveq2d | |
7 | eqid | |
|
8 | 1on | |
|
9 | 8 | a1i | |
10 | id | |
|
11 | 7 9 10 | mplsca | |
12 | 11 | fveq2d | |
13 | eqid | |
|
14 | 1 7 13 | ply1vsca | |
15 | 14 | a1i | |
16 | 15 | oveqdr | |
17 | eqid | |
|
18 | 7 1 17 | ply1mpl1 | |
19 | 18 | a1i | |
20 | fvexd | |
|
21 | 3 4 6 12 16 19 20 | asclpropd | |
22 | fvprc | |
|
23 | 1 22 | eqtrid | |
24 | reldmmpl | |
|
25 | 24 | ovprc2 | |
26 | 23 25 | eqtr4d | |
27 | 26 | fveq2d | |
28 | 21 27 | pm2.61i | |
29 | 2 28 | eqtri | |