Metamath Proof Explorer


Theorem rimrhm

Description: A ring isomorphism is a homomorphism. Compare gimghm . (Contributed by AV, 22-Oct-2019) Remove hypotheses. (Revised by SN, 10-Jan-2025)

Ref Expression
Assertion rimrhm F R RingIso S F R RingHom S

Proof

Step Hyp Ref Expression
1 isrim0 F R RingIso S F R RingHom S F -1 S RingHom R
2 1 simplbi F R RingIso S F R RingHom S