Metamath Proof Explorer

Theorem brric2

Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to Definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)

		Ref	Expression
	Assertion	brric2	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$

Proof

Step	Hyp	Ref	Expression
1		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
2		n0	$⊢ R RingIso S \neq \emptyset \leftrightarrow \exists f f \in (R RingIso S)$
3		rimrcl	$⊢ f \in (R RingIso S) \to (R \in V \land S \in V)$
4		isrim0	$⊢ (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)))$
5		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
6		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
7	5 6	isrhm	$⊢ f \in (R RingHom S) \leftrightarrow ((R \in Ring \land S \in Ring) \land (f \in (R GrpHom S) \land f \in ({mulGrp}_{R} MndHom {mulGrp}_{S})))$
8	7	simplbi	$⊢ f \in (R RingHom S) \to (R \in Ring \land S \in Ring)$
9	8	adantr	$⊢ (f \in (R RingHom S) \land f^{-1} \in (S RingHom R)) \to (R \in Ring \land S \in Ring)$
10	4 9	syl6bi	$⊢ (R \in V \land S \in V) \to (f \in (R RingIso S) \to (R \in Ring \land S \in Ring))$
11	3 10	mpcom	$⊢ f \in (R RingIso S) \to (R \in Ring \land S \in Ring)$
12	11	exlimiv	$⊢ \exists f f \in (R RingIso S) \to (R \in Ring \land S \in Ring)$
13	12	pm4.71ri	$⊢ \exists f f \in (R RingIso S) \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$
14	1 2 13	3bitri	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$