Metamath Proof Explorer

Theorem lmimcnv

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

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

Proof

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