Metamath Proof Explorer

Theorem srngring

Description: A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015)

Ref Expression
Assertion srngring 
|- ( R e. *Ring -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
2 eqid 
 |-  ( *rf ` R ) = ( *rf ` R )
3 1 2 srngrhm 
 |-  ( R e. *Ring -> ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) )
4 rhmrcl1 
 |-  ( ( *rf ` R ) e. ( R RingHom ( oppR ` R ) ) -> R e. Ring )
5 3 4 syl 
 |-  ( R e. *Ring -> R e. Ring )