| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1scl.p |
|- P = ( Poly1 ` R ) |
| 2 |
|
ply1scl.a |
|- A = ( algSc ` P ) |
| 3 |
|
ply1scl0.z |
|- .0. = ( 0g ` R ) |
| 4 |
|
ply1scl0.y |
|- Y = ( 0g ` P ) |
| 5 |
1
|
ply1sca |
|- ( R e. Ring -> R = ( Scalar ` P ) ) |
| 6 |
5
|
fveq2d |
|- ( R e. Ring -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) ) |
| 7 |
3 6
|
eqtrid |
|- ( R e. Ring -> .0. = ( 0g ` ( Scalar ` P ) ) ) |
| 8 |
7
|
fveq2d |
|- ( R e. Ring -> ( A ` .0. ) = ( A ` ( 0g ` ( Scalar ` P ) ) ) ) |
| 9 |
|
eqid |
|- ( Scalar ` P ) = ( Scalar ` P ) |
| 10 |
1
|
ply1lmod |
|- ( R e. Ring -> P e. LMod ) |
| 11 |
1
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
| 12 |
2 9 10 11
|
ascl0 |
|- ( R e. Ring -> ( A ` ( 0g ` ( Scalar ` P ) ) ) = ( 0g ` P ) ) |
| 13 |
8 12
|
eqtrd |
|- ( R e. Ring -> ( A ` .0. ) = ( 0g ` P ) ) |
| 14 |
13 4
|
eqtr4di |
|- ( R e. Ring -> ( A ` .0. ) = Y ) |