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

Proof

Step Hyp Ref Expression
1 ricdrng1 
 |-  ( ( R ~=r S /\ R e. DivRing ) -> S e. DivRing )
2 ricsym 
 |-  ( R ~=r S -> S ~=r R )
3 ricdrng1 
 |-  ( ( S ~=r R /\ S e. DivRing ) -> R e. DivRing )
4 2 3 sylan 
 |-  ( ( R ~=r S /\ S e. DivRing ) -> R e. DivRing )
5 1 4 impbida 
 |-  ( R ~=r S -> ( R e. DivRing <-> S e. DivRing ) )