Metamath Proof Explorer

Theorem drngdomn

Description: A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015)

Ref Expression
Assertion drngdomn 
|- ( R e. DivRing -> R e. Domn )

Proof

Step Hyp Ref Expression
1 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 2 3 4 isdrng 
 |-  ( R e. DivRing <-> ( R e. Ring /\ ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) ) )
6 5 simprbi 
 |-  ( R e. DivRing -> ( Unit ` R ) = ( ( Base ` R ) \ { ( 0g ` R ) } ) )
7 drngring 
 |-  ( R e. DivRing -> R e. Ring )
8 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
9 8 3 unitrrg 
 |-  ( R e. Ring -> ( Unit ` R ) C_ ( RLReg ` R ) )
10 7 9 syl 
 |-  ( R e. DivRing -> ( Unit ` R ) C_ ( RLReg ` R ) )
11 6 10 eqsstrrd 
 |-  ( R e. DivRing -> ( ( Base ` R ) \ { ( 0g ` R ) } ) C_ ( RLReg ` R ) )
12 2 8 4 isdomn2 
 |-  ( R e. Domn <-> ( R e. NzRing /\ ( ( Base ` R ) \ { ( 0g ` R ) } ) C_ ( RLReg ` R ) ) )
13 1 11 12 sylanbrc 
 |-  ( R e. DivRing -> R e. Domn )