This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ricdomn

Description: A ring is a domain if and only if an isomorphic ring is a domain. (Contributed by Thierry Arnoux, 4-May-2026)

		Ref	Expression
	Assertion	ricdomn	$⊢ R ≃_{𝑟} S \to (R \in Domn \leftrightarrow S \in Domn)$

Step	Hyp	Ref	Expression
1		ricdomn1	$⊢ (R ≃_{𝑟} S \land R \in Domn) \to S \in Domn$
2		ricsym	$⊢ R ≃_{𝑟} S \to S ≃_{𝑟} R$
3		ricdomn1	$⊢ (S ≃_{𝑟} R \land S \in Domn) \to R \in Domn$
4	2 3	sylan	$⊢ (R ≃_{𝑟} S \land S \in Domn) \to R \in Domn$
5	1 4	impbida	$⊢ R ≃_{𝑟} S \to (R \in Domn \leftrightarrow S \in Domn)$