Metamath Proof Explorer

Theorem orngring

Description: An ordered ring is a ring. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion orngring 
|- ( R e. oRing -> R e. Ring )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` R ) = ( Base ` R )
2 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
3 eqid 
 |-  ( .r ` R ) = ( .r ` R )
4 eqid 
 |-  ( le ` R ) = ( le ` R )
5 1 2 3 4 isorng 
 |-  ( R e. oRing <-> ( R e. Ring /\ R e. oGrp /\ A. a e. ( Base ` R ) A. b e. ( Base ` R ) ( ( ( 0g ` R ) ( le ` R ) a /\ ( 0g ` R ) ( le ` R ) b ) -> ( 0g ` R ) ( le ` R ) ( a ( .r ` R ) b ) ) ) )
6 5 simp1bi 
 |-  ( R e. oRing -> R e. Ring )