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 e. ( R RingIso S ) -> F e. ( R RingHom S ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isrim0 | |- ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) ) |
|
2 | 1 | simplbi | |- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) ) |