Step |
Hyp |
Ref |
Expression |
1 |
|
opsrring.o |
|- O = ( ( I ordPwSer R ) ` T ) |
2 |
|
opsrring.i |
|- ( ph -> I e. V ) |
3 |
|
opsrring.r |
|- ( ph -> R e. Ring ) |
4 |
|
opsrring.t |
|- ( ph -> T C_ ( I X. I ) ) |
5 |
|
eqid |
|- ( I mPwSer R ) = ( I mPwSer R ) |
6 |
5 2 3
|
psrring |
|- ( ph -> ( I mPwSer R ) e. Ring ) |
7 |
|
eqidd |
|- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) ) |
8 |
5 1 4
|
opsrbas |
|- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` O ) ) |
9 |
5 1 4
|
opsrplusg |
|- ( ph -> ( +g ` ( I mPwSer R ) ) = ( +g ` O ) ) |
10 |
9
|
oveqdr |
|- ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( +g ` ( I mPwSer R ) ) y ) = ( x ( +g ` O ) y ) ) |
11 |
5 1 4
|
opsrmulr |
|- ( ph -> ( .r ` ( I mPwSer R ) ) = ( .r ` O ) ) |
12 |
11
|
oveqdr |
|- ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( .r ` ( I mPwSer R ) ) y ) = ( x ( .r ` O ) y ) ) |
13 |
7 8 10 12
|
ringpropd |
|- ( ph -> ( ( I mPwSer R ) e. Ring <-> O e. Ring ) ) |
14 |
6 13
|
mpbid |
|- ( ph -> O e. Ring ) |