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

Proof

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