isrngim2

Description: An isomorphism of non-unital rings is a bijective homomorphism. (Contributed by AV, 23-Feb-2020)

	Ref	Expression
Hypotheses	rnghmf1o.b	$⊢ B = {Base}_{R}$
	rnghmf1o.c	$⊢ C = {Base}_{S}$
Assertion	isrngim2	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C))$

Step	Hyp	Ref	Expression
1		rnghmf1o.b	$⊢ B = {Base}_{R}$
2		rnghmf1o.c	$⊢ C = {Base}_{S}$
3		isrngim	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F^{-1} \in (S RngHom R)))$
4	1 2	rnghmf1o	$⊢ F \in (R RngHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S RngHom R))$
5	4	bicomd	$⊢ F \in (R RngHom S) \to (F^{-1} \in (S RngHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
6	5	a1i	$⊢ (R \in V \land S \in W) \to (F \in (R RngHom S) \to (F^{-1} \in (S RngHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C))$
7	6	pm5.32d	$⊢ (R \in V \land S \in W) \to ((F \in (R RngHom S) \land F^{-1} \in (S RngHom R)) \leftrightarrow (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C))$
8	3 7	bitrd	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F : B \underset{1-1 onto}{⟶} C))$

Metamath Proof Explorer