isrngim

Description: An isomorphism of non-unital rings is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Feb-2020)

		Ref	Expression
	Assertion	isrngim	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F^{-1} \in (S RngHom R)))$

Proof

Step	Hyp	Ref	Expression
1		df-rngim	$⊢ RngIso = (r \in V, s \in V ⟼ \{f \in (r RngHom s) \| f^{-1} \in (s RngHom r)\})$
2	1	a1i	$⊢ (R \in V \land S \in W) \to RngIso = (r \in V, s \in V ⟼ \{f \in (r RngHom s) \| f^{-1} \in (s RngHom r)\})$
3		oveq12	$⊢ (r = R \land s = S) \to r RngHom s = R RngHom S$
4	3	adantl	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to r RngHom s = R RngHom S$
5		oveq12	$⊢ (s = S \land r = R) \to s RngHom r = S RngHom R$
6	5	ancoms	$⊢ (r = R \land s = S) \to s RngHom r = S RngHom R$
7	6	adantl	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to s RngHom r = S RngHom R$
8	7	eleq2d	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to (f^{-1} \in (s RngHom r) \leftrightarrow f^{-1} \in (S RngHom R))$
9	4 8	rabeqbidv	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to \{f \in (r RngHom s) \| f^{-1} \in (s RngHom r)\} = \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\}$
10		elex	$⊢ R \in V \to R \in V$
11	10	adantr	$⊢ (R \in V \land S \in W) \to R \in V$
12		elex	$⊢ S \in W \to S \in V$
13	12	adantl	$⊢ (R \in V \land S \in W) \to S \in V$
14		ovex	$⊢ R RngHom S \in V$
15	14	rabex	$⊢ \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\} \in V$
16	15	a1i	$⊢ (R \in V \land S \in W) \to \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\} \in V$
17	2 9 11 13 16	ovmpod	$⊢ (R \in V \land S \in W) \to R RngIso S = \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\}$
18	17	eleq2d	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow F \in \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\})$
19		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
20	19	eleq1d	$⊢ f = F \to (f^{-1} \in (S RngHom R) \leftrightarrow F^{-1} \in (S RngHom R))$
21	20	elrab	$⊢ F \in \{f \in (R RngHom S) \| f^{-1} \in (S RngHom R)\} \leftrightarrow (F \in (R RngHom S) \land F^{-1} \in (S RngHom R))$
22	18 21	bitrdi	$⊢ (R \in V \land S \in W) \to (F \in (R RngIso S) \leftrightarrow (F \in (R RngHom S) \land F^{-1} \in (S RngHom R)))$

Metamath Proof Explorer

Theorem isrngim

Proof