isrim0OLD

Description: Obsolete version of isrim0 as of 12-Jan-2025. (Contributed by AV, 22-Oct-2019) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-rim	$⊢ RingIso = (r \in V, s \in V ⟼ \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\})$
2	1	a1i	$⊢ (R \in V \land S \in W) \to RingIso = (r \in V, s \in V ⟼ \{f \in (r RingHom s) \| f^{-1} \in (s RingHom r)\})$
3		oveq12	$⊢ (r = R \land s = S) \to r RingHom s = R RingHom S$
4	3	adantl	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to r RingHom s = R RingHom S$
5		oveq12	$⊢ (s = S \land r = R) \to s RingHom r = S RingHom R$
6	5	ancoms	$⊢ (r = R \land s = S) \to s RingHom r = S RingHom R$
7	6	adantl	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to s RingHom r = S RingHom R$
8	7	eleq2d	$⊢ ((R \in V \land S \in W) \land (r = R \land s = S)) \to (f^{-1} \in (s RingHom r) \leftrightarrow f^{-1} \in (S RingHom R))$
9	4 8	rabeqbidv	$⊢ ((R \in V \land S \in W) \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)\}$
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 RingHom S \in V$
15	14	rabex	$⊢ \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\} \in V$
16	15	a1i	$⊢ (R \in V \land S \in W) \to \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\} \in V$
17	2 9 11 13 16	ovmpod	$⊢ (R \in V \land S \in W) \to R RingIso S = \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\}$
18	17	eleq2d	$⊢ (R \in V \land S \in W) \to (F \in (R RingIso S) \leftrightarrow F \in \{f \in (R RingHom S) \| f^{-1} \in (S RingHom R)\})$
19		cnveq	$⊢ f = F \to f^{-1} = F^{-1}$
20	19	eleq1d	$⊢ f = F \to (f^{-1} \in (S RingHom R) \leftrightarrow F^{-1} \in (S RingHom R))$
21	20	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))$
22	18 21	bitrdi	$⊢ (R \in V \land S \in W) \to (F \in (R RingIso S) \leftrightarrow (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)))$

Metamath Proof Explorer

Theorem isrim0OLD

Proof