Metamath Proof Explorer

Theorem drngring

Description: A division ring is a ring. (Contributed by NM, 8-Sep-2011)

Ref Expression
Assertion drngring 
|- ( R e. DivRing -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 1 2 3 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) )
5 4 simplbi 
 |-  ( R e. DivRing -> R e. Ring )