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

Metamath Proof Explorer

Theorem opprringb

Description: Bidirectional form of opprring . (Contributed by Mario Carneiro, 6-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 opprbas.1 
 |-  O = ( oppR ` R )
2 1 opprring 
 |-  ( R e. Ring -> O e. Ring )
3 eqid 
 |-  ( oppR ` O ) = ( oppR ` O )
4 3 opprring 
 |-  ( O e. Ring -> ( oppR ` O ) e. Ring )
5 eqidd 
 |-  ( T. -> ( Base ` R ) = ( Base ` R ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 1 6 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
8 3 7 opprbas 
 |-  ( Base ` R ) = ( Base ` ( oppR ` O ) )
9 8 a1i 
 |-  ( T. -> ( Base ` R ) = ( Base ` ( oppR ` O ) ) )
10 eqid 
 |-  ( +g ` R ) = ( +g ` R )
11 1 10 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
12 3 11 oppradd 
 |-  ( +g ` R ) = ( +g ` ( oppR ` O ) )
13 12 oveqi 
 |-  ( x ( +g ` R ) y ) = ( x ( +g ` ( oppR ` O ) ) y )
14 13 a1i 
 |-  ( ( T. /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( +g ` R ) y ) = ( x ( +g ` ( oppR ` O ) ) y ) )
15 eqid 
 |-  ( .r ` O ) = ( .r ` O )
16 eqid 
 |-  ( .r ` ( oppR ` O ) ) = ( .r ` ( oppR ` O ) )
17 7 15 3 16 opprmul 
 |-  ( x ( .r ` ( oppR ` O ) ) y ) = ( y ( .r ` O ) x )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 6 18 1 15 opprmul 
 |-  ( y ( .r ` O ) x ) = ( x ( .r ` R ) y )
20 17 19 eqtr2i 
 |-  ( x ( .r ` R ) y ) = ( x ( .r ` ( oppR ` O ) ) y )
21 20 a1i 
 |-  ( ( T. /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( x ( .r ` R ) y ) = ( x ( .r ` ( oppR ` O ) ) y ) )
22 5 9 14 21 ringpropd 
 |-  ( T. -> ( R e. Ring <-> ( oppR ` O ) e. Ring ) )
23 22 mptru 
 |-  ( R e. Ring <-> ( oppR ` O ) e. Ring )
24 4 23 sylibr 
 |-  ( O e. Ring -> R e. Ring )
25 2 24 impbii 
 |-  ( R e. Ring <-> O e. Ring )