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

Metamath Proof Explorer

Theorem isrim

Description: An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019) Remove sethood antecedent. (Revised by SN, 12-Jan-2025)

Ref Expression
Hypotheses rhmf1o.b 
|- B = ( Base ` R )
rhmf1o.c 
|- C = ( Base ` S )
Assertion isrim 
|- ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) )

Proof

Step Hyp Ref Expression
1 rhmf1o.b 
 |-  B = ( Base ` R )
2 rhmf1o.c 
 |-  C = ( Base ` S )
3 isrim0 
 |-  ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) )
4 1 2 rhmf1o 
 |-  ( F e. ( R RingHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RingHom R ) ) )
5 4 bicomd 
 |-  ( F e. ( R RingHom S ) -> ( `' F e. ( S RingHom R ) <-> F : B -1-1-onto-> C ) )
6 5 pm5.32i 
 |-  ( ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) )
7 3 6 bitri 
 |-  ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) )