This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in (R RingIso S) \to F \in (R RingHom S)$

Proof

Step	Hyp	Ref	Expression
1		isrim0	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R))$
2	1	simplbi	$⊢ F \in (R RingIso S) \to F \in (R RingHom S)$