Metamath Proof Explorer

Theorem divrngpr

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

Ref Expression
Assertion divrngpr 
|- ( R e. DivRingOps -> R e. PrRing )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
3 eqid 
 |-  ( GId ` ( 1st ` R ) ) = ( GId ` ( 1st ` R ) )
4 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
5 1 2 3 4 isdrngo1 
 |-  ( R e. DivRingOps <-> ( R e. RingOps /\ ( ( 2nd ` R ) |` ( ( ran ( 1st ` R ) \ { ( GId ` ( 1st ` R ) ) } ) X. ( ran ( 1st ` R ) \ { ( GId ` ( 1st ` R ) ) } ) ) ) e. GrpOp ) )
6 5 simplbi 
 |-  ( R e. DivRingOps -> R e. RingOps )
7 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
8 1 2 4 3 7 dvrunz 
 |-  ( R e. DivRingOps -> ( GId ` ( 2nd ` R ) ) =/= ( GId ` ( 1st ` R ) ) )
9 1 2 4 3 divrngidl 
 |-  ( R e. DivRingOps -> ( Idl ` R ) = { { ( GId ` ( 1st ` R ) ) } , ran ( 1st ` R ) } )
10 1 2 4 3 7 smprngopr 
 |-  ( ( R e. RingOps /\ ( GId ` ( 2nd ` R ) ) =/= ( GId ` ( 1st ` R ) ) /\ ( Idl ` R ) = { { ( GId ` ( 1st ` R ) ) } , ran ( 1st ` R ) } ) -> R e. PrRing )
11 6 8 9 10 syl3anc 
 |-  ( R e. DivRingOps -> R e. PrRing )