rimcnv

Description: The converse of a ring isomorphism is a ring isomorphism. (Contributed by SN, 10-Jan-2025)

		Ref	Expression
	Assertion	rimcnv	$⊢ F \in (R RingIso S) \to F^{-1} \in (S RingIso R)$

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

Metamath Proof Explorer