| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ply1ascl0.w |
|- W = ( Poly1 ` R ) |
| 2 |
|
ply1ascl0.a |
|- A = ( algSc ` W ) |
| 3 |
|
ply1ascl0.o |
|- O = ( 0g ` R ) |
| 4 |
|
ply1ascl0.1 |
|- .0. = ( 0g ` W ) |
| 5 |
|
ply1ascl0.r |
|- ( ph -> R e. Ring ) |
| 6 |
1
|
ply1sca |
|- ( R e. Ring -> R = ( Scalar ` W ) ) |
| 7 |
5 6
|
syl |
|- ( ph -> R = ( Scalar ` W ) ) |
| 8 |
7
|
fveq2d |
|- ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` W ) ) ) |
| 9 |
3 8
|
eqtrid |
|- ( ph -> O = ( 0g ` ( Scalar ` W ) ) ) |
| 10 |
9
|
fveq2d |
|- ( ph -> ( ( algSc ` W ) ` O ) = ( ( algSc ` W ) ` ( 0g ` ( Scalar ` W ) ) ) ) |
| 11 |
|
eqid |
|- ( algSc ` W ) = ( algSc ` W ) |
| 12 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 13 |
1
|
ply1lmod |
|- ( R e. Ring -> W e. LMod ) |
| 14 |
5 13
|
syl |
|- ( ph -> W e. LMod ) |
| 15 |
1
|
ply1ring |
|- ( R e. Ring -> W e. Ring ) |
| 16 |
5 15
|
syl |
|- ( ph -> W e. Ring ) |
| 17 |
11 12 14 16
|
ascl0 |
|- ( ph -> ( ( algSc ` W ) ` ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` W ) ) |
| 18 |
10 17
|
eqtrd |
|- ( ph -> ( ( algSc ` W ) ` O ) = ( 0g ` W ) ) |
| 19 |
2
|
fveq1i |
|- ( A ` O ) = ( ( algSc ` W ) ` O ) |
| 20 |
18 19 4
|
3eqtr4g |
|- ( ph -> ( A ` O ) = .0. ) |