Metamath Proof Explorer

Theorem drngprmrng

Description: A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 18-Jun-2026)

Ref Expression
Assertion drngprmrng 
|- ( R e. DivRing -> R e. PrmRing )

Proof

Step Hyp Ref Expression
1 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 2 3 4 drngnidl 
 |-  ( R e. DivRing -> ( LIdeal ` R ) = { { ( 0g ` R ) } , ( Base ` R ) } )
6 2 3 4 smprngprmrng 
 |-  ( ( R e. NzRing /\ ( LIdeal ` R ) = { { ( 0g ` R ) } , ( Base ` R ) } ) -> R e. PrmRing )
7 1 5 6 syl2anc 
 |-  ( R e. DivRing -> R e. PrmRing )