Metamath Proof Explorer

Theorem ricdrng

Description: A ring is a division ring if and only if an isomorphic ring is a division ring. (Contributed by SN, 18-Feb-2025)

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

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