| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sral1r.a |
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) ) |
| 2 |
|
sral1r.1 |
|- ( ph -> .1. = ( 1r ` W ) ) |
| 3 |
|
sral1r.s |
|- ( ph -> S C_ ( Base ` W ) ) |
| 4 |
|
eqidd |
|- ( ph -> ( Base ` W ) = ( Base ` W ) ) |
| 5 |
1 3
|
srabase |
|- ( ph -> ( Base ` W ) = ( Base ` A ) ) |
| 6 |
1 3
|
sramulr |
|- ( ph -> ( .r ` W ) = ( .r ` A ) ) |
| 7 |
6
|
oveqdr |
|- ( ( ph /\ ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( x ( .r ` W ) y ) = ( x ( .r ` A ) y ) ) |
| 8 |
4 5 7
|
rngidpropd |
|- ( ph -> ( 1r ` W ) = ( 1r ` A ) ) |
| 9 |
2 8
|
eqtrd |
|- ( ph -> .1. = ( 1r ` A ) ) |