Metamath Proof Explorer

Theorem isprrngo

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

Ref Expression
Hypotheses isprrng.1 
|- G = ( 1st ` R )
isprrng.2 
|- Z = ( GId ` G )
Assertion isprrngo 
|- ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )

Proof

Step Hyp Ref Expression
1 isprrng.1 
 |-  G = ( 1st ` R )
2 isprrng.2 
 |-  Z = ( GId ` G )
3 fveq2 
 |-  ( r = R -> ( 1st ` r ) = ( 1st ` R ) )
4 3 1 eqtr4di 
 |-  ( r = R -> ( 1st ` r ) = G )
5 4 fveq2d 
 |-  ( r = R -> ( GId ` ( 1st ` r ) ) = ( GId ` G ) )
6 5 2 eqtr4di 
 |-  ( r = R -> ( GId ` ( 1st ` r ) ) = Z )
7 6 sneqd 
 |-  ( r = R -> { ( GId ` ( 1st ` r ) ) } = { Z } )
8 fveq2 
 |-  ( r = R -> ( PrIdl ` r ) = ( PrIdl ` R ) )
9 7 8 eleq12d 
 |-  ( r = R -> ( { ( GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) <-> { Z } e. ( PrIdl ` R ) ) )
10 df-prrngo 
 |-  PrRing = { r e. RingOps | { ( GId ` ( 1st ` r ) ) } e. ( PrIdl ` r ) }
11 9 10 elrab2 
 |-  ( R e. PrRing <-> ( R e. RingOps /\ { Z } e. ( PrIdl ` R ) ) )