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 ~=r S -> ( R e. Field <-> S e. Field ) )

Proof

Step Hyp Ref Expression
1 ricdrng 
 |-  ( R ~=r S -> ( R e. DivRing <-> S e. DivRing ) )
2 riccrng 
 |-  ( R ~=r S -> ( R e. CRing <-> S e. CRing ) )
3 1 2 anbi12d 
 |-  ( R ~=r S -> ( ( R e. DivRing /\ R e. CRing ) <-> ( S e. DivRing /\ S e. CRing ) ) )
4 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
5 isfld 
 |-  ( S e. Field <-> ( S e. DivRing /\ S e. CRing ) )
6 3 4 5 3bitr4g 
 |-  ( R ~=r S -> ( R e. Field <-> S e. Field ) )