Metamath Proof Explorer

Theorem rhmrcl1

Description: Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion rhmrcl1 
|- ( F e. ( R RingHom S ) -> R e. Ring )

Proof

Step Hyp Ref Expression
1 dfrhm2 
 |-  RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) )
2 1 elmpocl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )