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	⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑅 ∈ CRing ↔ 𝑆 ∈ CRing ) )

Proof

Step	Hyp	Ref	Expression
1		riccrng1	⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing )
2		ricsym	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑆 ≃𝑟 𝑅 )
3		riccrng1	⊢ ( ( 𝑆 ≃𝑟 𝑅 ∧ 𝑆 ∈ CRing ) → 𝑅 ∈ CRing )
4	2 3	sylan	⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑆 ∈ CRing ) → 𝑅 ∈ CRing )
5	1 4	impbida	⊢ ( 𝑅 ≃𝑟 𝑆 → ( 𝑅 ∈ CRing ↔ 𝑆 ∈ CRing ) )