Metamath Proof Explorer

Theorem prrngorngo

Description: A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion prrngorngo 
|- ( R e. PrRing -> R e. RingOps )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
2 eqid 
 |-  ( GId ` ( 1st ` R ) ) = ( GId ` ( 1st ` R ) )
3 1 2 isprrngo 
 |-  ( R e. PrRing <-> ( R e. RingOps /\ { ( GId ` ( 1st ` R ) ) } e. ( PrIdl ` R ) ) )
4 3 simplbi 
 |-  ( R e. PrRing -> R e. RingOps )