| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mplascl1.w |
|- W = ( I mPoly R ) |
| 2 |
|
mplascl1.a |
|- A = ( algSc ` W ) |
| 3 |
|
mplascl1.o |
|- O = ( 1r ` R ) |
| 4 |
|
mplascl1.1 |
|- .1. = ( 1r ` W ) |
| 5 |
|
mplascl1.i |
|- ( ph -> I e. V ) |
| 6 |
|
mplascl1.r |
|- ( ph -> R e. Ring ) |
| 7 |
1 5 6
|
mplsca |
|- ( ph -> R = ( Scalar ` W ) ) |
| 8 |
7
|
fveq2d |
|- ( ph -> ( 1r ` R ) = ( 1r ` ( Scalar ` W ) ) ) |
| 9 |
3 8
|
eqtrid |
|- ( ph -> O = ( 1r ` ( Scalar ` W ) ) ) |
| 10 |
9
|
fveq2d |
|- ( ph -> ( A ` O ) = ( A ` ( 1r ` ( 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
|
ascl1 |
|- ( ph -> ( A ` ( 1r ` ( Scalar ` W ) ) ) = ( 1r ` W ) ) |
| 15 |
10 14
|
eqtrd |
|- ( ph -> ( A ` O ) = ( 1r ` W ) ) |
| 16 |
15 4
|
eqtr4di |
|- ( ph -> ( A ` O ) = .1. ) |