| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mplascl0.w |
|- W = ( I mPoly R ) |
| 2 |
|
mplascl0.a |
|- A = ( algSc ` W ) |
| 3 |
|
mplascl0.o |
|- O = ( 0g ` R ) |
| 4 |
|
mplascl0.0 |
|- .0. = ( 0g ` W ) |
| 5 |
|
mplascl0.i |
|- ( ph -> I e. V ) |
| 6 |
|
mplascl0.r |
|- ( ph -> R e. Ring ) |
| 7 |
1 5 6
|
mplsca |
|- ( 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 -> ( A ` O ) = ( A ` ( 0g ` ( Scalar ` W ) ) ) ) |
| 11 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 12 |
1 5 6
|
mpllmodd |
|- ( ph -> W e. LMod ) |
| 13 |
1 5 6
|
mplringd |
|- ( ph -> W e. Ring ) |
| 14 |
2 11 12 13
|
ascl0 |
|- ( ph -> ( A ` ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` W ) ) |
| 15 |
10 14
|
eqtrd |
|- ( ph -> ( A ` O ) = ( 0g ` W ) ) |
| 16 |
15 4
|
eqtr4di |
|- ( ph -> ( A ` O ) = .0. ) |