Metamath Proof Explorer

Theorem riccrng

Description: A ring is commutative if and only if an isomorphic ring is commutative. (Contributed by SN, 10-Jan-2025)

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

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