isrim0

Description: A ring isomorphism is a homomorphism whose converse is also a homomorphism. Compare isgim2 . (Contributed by AV, 22-Oct-2019) Remove sethood antecedent. (Revised by SN, 10-Jan-2025)

		Ref	Expression
	Assertion	isrim0	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R))$

Proof

Step	Hyp	Ref	Expression
1		rimrcl	$⊢ F \in (R RingIso S) \to (R \in V \land S \in V)$
2		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
3	2	elexd	$⊢ F \in (R RingHom S) \to R \in V$
4		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
5	4	elexd	$⊢ F \in (R RingHom S) \to S \in V$
6	3 5	jca	$⊢ F \in (R RingHom S) \to (R \in V \land S \in V)$
7	6	adantr	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to (R \in V \land S \in V)$
8		df-rim	$⊢ RingIso = (r \in V, s \in V ⟼ \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\})$
9	8	a1i	$⊢ (R \in V \land S \in V) \to RingIso = (r \in V, s \in V ⟼ \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\})$
10		oveq12	$⊢ (r = R \land s = S) \to r RingHom s = R RingHom S$
11	10	adantl	$⊢ ((R \in V \land S \in V) \land (r = R \land s = S)) \to r RingHom s = R RingHom S$
12		oveq12	$⊢ (s = S \land r = R) \to s RingHom r = S RingHom R$
13	12	ancoms	$⊢ (r = R \land s = S) \to s RingHom r = S RingHom R$
14	13	adantl	$⊢ ((R \in V \land S \in V) \land (r = R \land s = S)) \to s RingHom r = S RingHom R$
15	14	eleq2d	$⊢ ((R \in V \land S \in V) \land (r = R \land s = S)) \to (f^{-1} \in (s RingHom r) \leftrightarrow f^{-1} \in (S RingHom R))$
16	11 15	rabeqbidv	$⊢ ((R \in V \land S \in V) \land (r = R \land s = S)) \to \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\} = \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\}$
17		simpl	$⊢ (R \in V \land S \in V) \to R \in V$
18		simpr	$⊢ (R \in V \land S \in V) \to S \in V$
19		ovex	$⊢ R RingHom S \in V$
20	19	rabex	$⊢ \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\} \in V$
21	20	a1i	$⊢ (R \in V \land S \in V) \to \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\} \in V$
22	9 16 17 18 21	ovmpod	$⊢ (R \in V \land S \in V) \to R RingIso S = \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\}$
23	22	eleq2d	$⊢ (R \in V \land S \in V) \to (F \in (R RingIso S) \leftrightarrow F \in \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\})$
24		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
25	24	eleq1d	$⊢ f = F \to (f^{-1} \in (S RingHom R) \leftrightarrow F^{-1} \in (S RingHom R))$
26	25	elrab	$⊢ F \in \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\} \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R))$
27	23 26	bitrdi	$⊢ (R \in V \land S \in V) \to (F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)))$
28	1 7 27	pm5.21nii	$⊢ F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R))$

Metamath Proof Explorer

Theorem isrim0

Proof