Metamath Proof Explorer

Theorem isgim2

Description: A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo . (Contributed by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	isgim2	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F^{-1} \in (S GrpHom R))$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{R} = {Base}_{R}$
2		eqid	$⊢ {Base}_{S} = {Base}_{S}$
3	1 2	isgim	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
4	1 2	ghmf1o	$⊢ F \in (R GrpHom S) \to (F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \leftrightarrow F^{-1} \in (S GrpHom R))$
5	4	pm5.32i	$⊢ (F \in (R GrpHom S) \land F : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}) \leftrightarrow (F \in (R GrpHom S) \land F^{-1} \in (S GrpHom R))$
6	3 5	bitri	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F^{-1} \in (S GrpHom R))$