Metamath Proof Explorer


Theorem ricfld

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

Ref Expression
Assertion ricfld R 𝑟 S R Field S Field

Proof

Step Hyp Ref Expression
1 ricdrng R 𝑟 S R DivRing S DivRing
2 riccrng R 𝑟 S R CRing S CRing
3 1 2 anbi12d R 𝑟 S R DivRing R CRing S DivRing S CRing
4 isfld R Field R DivRing R CRing
5 isfld S Field S DivRing S CRing
6 3 4 5 3bitr4g R 𝑟 S R Field S Field