Metamath Proof Explorer


Theorem opprring

Description: An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Aug-2015) (Proof shortened by AV, 30-Mar-2025)

Ref Expression
Hypothesis opprbas.1
|- O = ( oppR ` R )
Assertion opprring
|- ( R e. Ring -> O e. Ring )

Proof

Step Hyp Ref Expression
1 opprbas.1
 |-  O = ( oppR ` R )
2 ringrng
 |-  ( R e. Ring -> R e. Rng )
3 1 opprrng
 |-  ( R e. Rng -> O e. Rng )
4 2 3 syl
 |-  ( R e. Ring -> O e. Rng )
5 oveq1
 |-  ( z = ( 1r ` R ) -> ( z ( .r ` O ) x ) = ( ( 1r ` R ) ( .r ` O ) x ) )
6 5 eqeq1d
 |-  ( z = ( 1r ` R ) -> ( ( z ( .r ` O ) x ) = x <-> ( ( 1r ` R ) ( .r ` O ) x ) = x ) )
7 6 ovanraleqv
 |-  ( z = ( 1r ` R ) -> ( A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) <-> A. x e. ( Base ` R ) ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) ) )
8 eqid
 |-  ( Base ` R ) = ( Base ` R )
9 eqid
 |-  ( 1r ` R ) = ( 1r ` R )
10 8 9 ringidcl
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
11 eqid
 |-  ( .r ` R ) = ( .r ` R )
12 eqid
 |-  ( .r ` O ) = ( .r ` O )
13 8 11 1 12 opprmul
 |-  ( ( 1r ` R ) ( .r ` O ) x ) = ( x ( .r ` R ) ( 1r ` R ) )
14 8 11 9 ringridm
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 1r ` R ) ) = x )
15 13 14 eqtrid
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` O ) x ) = x )
16 8 11 1 12 opprmul
 |-  ( x ( .r ` O ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) x )
17 8 11 9 ringlidm
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x )
18 16 17 eqtrid
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` O ) ( 1r ` R ) ) = x )
19 15 18 jca
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) )
20 19 ralrimiva
 |-  ( R e. Ring -> A. x e. ( Base ` R ) ( ( ( 1r ` R ) ( .r ` O ) x ) = x /\ ( x ( .r ` O ) ( 1r ` R ) ) = x ) )
21 7 10 20 rspcedvdw
 |-  ( R e. Ring -> E. z e. ( Base ` R ) A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) )
22 1 8 opprbas
 |-  ( Base ` R ) = ( Base ` O )
23 22 12 isringrng
 |-  ( O e. Ring <-> ( O e. Rng /\ E. z e. ( Base ` R ) A. x e. ( Base ` R ) ( ( z ( .r ` O ) x ) = x /\ ( x ( .r ` O ) z ) = x ) ) )
24 4 21 23 sylanbrc
 |-  ( R e. Ring -> O e. Ring )