Metamath Proof Explorer

Theorem isrim

Description: An isomorphism of rings is a bijective homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 22-Oct-2019) Remove sethood antecedent. (Revised by SN, 12-Jan-2025)

		Ref	Expression
	Hypotheses	rhmf1o.b	$⊢ B = {Base}_{R}$
		rhmf1o.c	$⊢ C = {Base}_{S}$
	Assertion	isrim	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C)$

Proof

Step	Hyp	Ref	Expression
1		rhmf1o.b	$⊢ B = {Base}_{R}$
2		rhmf1o.c	$⊢ C = {Base}_{S}$
3		isrim0	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R))$
4	1 2	rhmf1o	$⊢ F \in (R RingHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S RingHom R))$
5	4	bicomd	$⊢ F \in (R RingHom S) \to (F^{-1} \in (S RingHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
6	5	pm5.32i	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \leftrightarrow (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C)$
7	3 6	bitri	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C)$