rngimcnv

Description: The converse of an isomorphism of non-unital rings is an isomorphism of non-unital rings. (Contributed by AV, 27-Feb-2025)

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

Step	Hyp	Ref	Expression
1		rngimrcl	$⊢ F \in (S RngIsom T) \to (S \in V \land T \in V)$
2		isrngisom	$⊢ (S \in V \land T \in V) \to (F \in (S RngIsom T) \leftrightarrow (F \in (S RngHomo T) \land F^{-1} \in (T RngHomo S)))$
3		eqid	$⊢ {Base}_{S} = {Base}_{S}$
4		eqid	$⊢ {Base}_{T} = {Base}_{T}$
5	3 4	rnghmf	$⊢ F \in (S RngHomo T) \to F : {Base}_{S} ⟶ {Base}_{T}$
6		frel	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to Rel F$
7		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
8	6 7	sylib	$⊢ F : {Base}_{S} ⟶ {Base}_{T} \to {F^{-1}}^{-1} = F$
9	5 8	syl	$⊢ F \in (S RngHomo T) \to {F^{-1}}^{-1} = F$
10		id	$⊢ F \in (S RngHomo T) \to F \in (S RngHomo T)$
11	9 10	eqeltrd	$⊢ F \in (S RngHomo T) \to {F^{-1}}^{-1} \in (S RngHomo T)$
12	11	anim1ci	$⊢ (F \in (S RngHomo T) \land F^{-1} \in (T RngHomo S)) \to (F^{-1} \in (T RngHomo S) \land {F^{-1}}^{-1} \in (S RngHomo T))$
13		isrngisom	$⊢ (T \in V \land S \in V) \to (F^{-1} \in (T RngIsom S) \leftrightarrow (F^{-1} \in (T RngHomo S) \land {F^{-1}}^{-1} \in (S RngHomo T)))$
14	13	ancoms	$⊢ (S \in V \land T \in V) \to (F^{-1} \in (T RngIsom S) \leftrightarrow (F^{-1} \in (T RngHomo S) \land {F^{-1}}^{-1} \in (S RngHomo T)))$
15	12 14	imbitrrid	$⊢ (S \in V \land T \in V) \to ((F \in (S RngHomo T) \land F^{-1} \in (T RngHomo S)) \to F^{-1} \in (T RngIsom S))$
16	2 15	sylbid	$⊢ (S \in V \land T \in V) \to (F \in (S RngIsom T) \to F^{-1} \in (T RngIsom S))$
17	1 16	mpcom	$⊢ F \in (S RngIsom T) \to F^{-1} \in (T RngIsom S)$

Metamath Proof Explorer