Metamath Proof Explorer

Theorem rngoisohom

Description: A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion rngoisohom 
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
3 eqid 
 |-  ( 1st ` S ) = ( 1st ` S )
4 eqid 
 |-  ran ( 1st ` S ) = ran ( 1st ` S )
5 1 2 3 4 isrngoiso 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RingOpsIso S ) <-> ( F e. ( R RingOpsHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) )
6 5 simprbda 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )
7 6 3impa 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> F e. ( R RingOpsHom S ) )