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 R DivRing S DivRing

Proof

Step Hyp Ref Expression
1 ricdrng1 R 𝑟 S R DivRing S DivRing
2 ricsym R 𝑟 S S 𝑟 R
3 ricdrng1 S 𝑟 R S DivRing R DivRing
4 2 3 sylan R 𝑟 S S DivRing R DivRing
5 1 4 impbida R 𝑟 S R DivRing S DivRing