Metamath Proof Explorer

Theorem isrimOLD

Description: Obsolete version of isrim as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	rhmf1o.b	$⊢ B = {Base}_{R}$
		rhmf1o.c	$⊢ C = {Base}_{S}$
	Assertion	isrimOLD	$⊢ (R \in V \land S \in W) \to (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		isrim0OLD	$⊢ (R \in V \land S \in W) \to (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	a1i	$⊢ (R \in V \land S \in W) \to (F \in (R RingHom S) \to (F^{-1} \in (S RingHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C))$
7	6	pm5.32d	$⊢ (R \in V \land S \in W) \to ((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))$
8	3 7	bitrd	$⊢ (R \in V \land S \in W) \to (F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C))$