Step |
Hyp |
Ref |
Expression |
1 |
|
brric |
|- ( R ~=r S <-> ( R RingIso S ) =/= (/) ) |
2 |
|
n0 |
|- ( ( R RingIso S ) =/= (/) <-> E. f f e. ( R RingIso S ) ) |
3 |
|
rimrhm |
|- ( f e. ( R RingIso S ) -> f e. ( R RingHom S ) ) |
4 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
5 |
|
eqid |
|- ( mulGrp ` S ) = ( mulGrp ` S ) |
6 |
4 5
|
isrhm |
|- ( f e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( f e. ( R GrpHom S ) /\ f e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) ) |
7 |
6
|
simplbi |
|- ( f e. ( R RingHom S ) -> ( R e. Ring /\ S e. Ring ) ) |
8 |
3 7
|
syl |
|- ( f e. ( R RingIso S ) -> ( R e. Ring /\ S e. Ring ) ) |
9 |
8
|
exlimiv |
|- ( E. f f e. ( R RingIso S ) -> ( R e. Ring /\ S e. Ring ) ) |
10 |
9
|
pm4.71ri |
|- ( E. f f e. ( R RingIso S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) ) |
11 |
1 2 10
|
3bitri |
|- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) ) |