This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brric2

Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion brric2 
|- ( R ~=r S <-> ( ( R e. Ring /\ S e. Ring ) /\ E. f f e. ( R RingIso S ) ) )

Proof

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 ) ) )