Description: Scalars of a univariate polynomial ring. (Contributed by Stefan O'Rear, 26-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ply1lmod.p | |
|
Assertion | ply1sca2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1lmod.p | |
|
2 | fvi | |
|
3 | 1 | ply1sca | |
4 | 2 3 | eqtrd | |
5 | fvprc | |
|
6 | fvprc | |
|
7 | 6 | fveq2d | |
8 | 1 | fveq2i | |
9 | scaid | |
|
10 | 9 | str0 | |
11 | 7 8 10 | 3eqtr4g | |
12 | 5 11 | eqtr4d | |
13 | 4 12 | pm2.61i | |