Metamath Proof Explorer


Theorem rimrhm

Description: An isomorphism of rings is a homomorphism. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses rhmf1o.b
|- B = ( Base ` R )
rhmf1o.c
|- C = ( Base ` S )
Assertion rimrhm
|- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) )

Proof

Step Hyp Ref Expression
1 rhmf1o.b
 |-  B = ( Base ` R )
2 rhmf1o.c
 |-  C = ( Base ` S )
3 rimrcl
 |-  ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )
4 1 2 isrim
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) ) )
5 simpl
 |-  ( ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) -> F e. ( R RingHom S ) )
6 4 5 syl6bi
 |-  ( ( R e. _V /\ S e. _V ) -> ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) ) )
7 3 6 mpcom
 |-  ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) )