Metamath Proof Explorer

Theorem gimcnv

Description: The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Assertion	gimcnv	$⊢ F \in (S GrpIso T) \to F^{-1} \in (T GrpIso S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{S} = {Base}_{S}$
2		eqid	$⊢ {Base}_{T} = {Base}_{T}$
3	1 2	ghmf	$⊢ F \in (S GrpHom T) \to F : {Base}_{S} ⟶ {Base}_{T}$
4		frel	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to Rel F$
5		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
6	4 5	sylib	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to {F^{-1}}^{-1} = F$
7	3 6	syl	$⊢ F \in (S GrpHom T) \to {F^{-1}}^{-1} = F$
8		id	$⊢ F \in (S GrpHom T) \to F \in (S GrpHom T)$
9	7 8	eqeltrd	$⊢ F \in (S GrpHom T) \to {F^{-1}}^{-1} \in (S GrpHom T)$
10	9	anim1ci	$⊢ (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S)) \to (F^{-1} \in (T GrpHom S) \land {F^{-1}}^{-1} \in (S GrpHom T))$
11		isgim2	$⊢ F \in (S GrpIso T) \leftrightarrow (F \in (S GrpHom T) \land F^{-1} \in (T GrpHom S))$
12		isgim2	$⊢ F^{-1} \in (T GrpIso S) \leftrightarrow (F^{-1} \in (T GrpHom S) \land {F^{-1}}^{-1} \in (S GrpHom T))$
13	10 11 12	3imtr4i	$⊢ F \in (S GrpIso T) \to F^{-1} \in (T GrpIso S)$