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		rimrhm	$⊢ f \in (R RingIso S) \to f \in (R RingHom S)$
4		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
5		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
6	4 5	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})))$
7	6	simplbi	$⊢ f \in (R RingHom S) \to (R \in Ring \land S \in Ring)$
8	3 7	syl	$⊢ f \in (R RingIso S) \to (R \in Ring \land S \in Ring)$
9	8	exlimiv	$⊢ \exists f f \in (R RingIso S) \to (R \in Ring \land S \in Ring)$
10	9	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))$
11	1 2 10	3bitri	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$