This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )