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)

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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 1 2 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
4 3 a1i 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` O ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 1 5 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
7 6 a1i 
 |-  ( R e. Ring -> ( +g ` R ) = ( +g ` O ) )
8 eqidd 
 |-  ( R e. Ring -> ( .r ` O ) = ( .r ` O ) )
9 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
10 3 6 grpprop 
 |-  ( R e. Grp <-> O e. Grp )
11 9 10 sylib 
 |-  ( R e. Ring -> O e. Grp )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 eqid 
 |-  ( .r ` O ) = ( .r ` O )
14 2 12 1 13 opprmul 
 |-  ( x ( .r ` O ) y ) = ( y ( .r ` R ) x )
15 2 12 ringcl 
 |-  ( ( R e. Ring /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( y ( .r ` R ) x ) e. ( Base ` R ) )
16 15 3com23 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( y ( .r ` R ) x ) e. ( Base ` R ) )
17 14 16 eqeltrid 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` O ) y ) e. ( Base ` R ) )
18 simpl 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> R e. Ring )
19 simpr3 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> z e. ( Base ` R ) )
20 simpr2 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> y e. ( Base ` R ) )
21 simpr1 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> x e. ( Base ` R ) )
22 2 12 ringass 
 |-  ( ( R e. Ring /\ ( z e. ( Base ` R ) /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) ) -> ( ( z ( .r ` R ) y ) ( .r ` R ) x ) = ( z ( .r ` R ) ( y ( .r ` R ) x ) ) )
23 18 19 20 21 22 syl13anc 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( z ( .r ` R ) y ) ( .r ` R ) x ) = ( z ( .r ` R ) ( y ( .r ` R ) x ) ) )
24 23 eqcomd 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( z ( .r ` R ) ( y ( .r ` R ) x ) ) = ( ( z ( .r ` R ) y ) ( .r ` R ) x ) )
25 14 oveq1i 
 |-  ( ( x ( .r ` O ) y ) ( .r ` O ) z ) = ( ( y ( .r ` R ) x ) ( .r ` O ) z )
26 2 12 1 13 opprmul 
 |-  ( ( y ( .r ` R ) x ) ( .r ` O ) z ) = ( z ( .r ` R ) ( y ( .r ` R ) x ) )
27 25 26 eqtri 
 |-  ( ( x ( .r ` O ) y ) ( .r ` O ) z ) = ( z ( .r ` R ) ( y ( .r ` R ) x ) )
28 2 12 1 13 opprmul 
 |-  ( y ( .r ` O ) z ) = ( z ( .r ` R ) y )
29 28 oveq2i 
 |-  ( x ( .r ` O ) ( y ( .r ` O ) z ) ) = ( x ( .r ` O ) ( z ( .r ` R ) y ) )
30 2 12 1 13 opprmul 
 |-  ( x ( .r ` O ) ( z ( .r ` R ) y ) ) = ( ( z ( .r ` R ) y ) ( .r ` R ) x )
31 29 30 eqtri 
 |-  ( x ( .r ` O ) ( y ( .r ` O ) z ) ) = ( ( z ( .r ` R ) y ) ( .r ` R ) x )
32 24 27 31 3eqtr4g 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( .r ` O ) y ) ( .r ` O ) z ) = ( x ( .r ` O ) ( y ( .r ` O ) z ) ) )
33 2 5 12 ringdir 
 |-  ( ( R e. Ring /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) /\ x e. ( Base ` R ) ) ) -> ( ( y ( +g ` R ) z ) ( .r ` R ) x ) = ( ( y ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) x ) ) )
34 18 20 19 21 33 syl13anc 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( y ( +g ` R ) z ) ( .r ` R ) x ) = ( ( y ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) x ) ) )
35 2 12 1 13 opprmul 
 |-  ( x ( .r ` O ) ( y ( +g ` R ) z ) ) = ( ( y ( +g ` R ) z ) ( .r ` R ) x )
36 2 12 1 13 opprmul 
 |-  ( x ( .r ` O ) z ) = ( z ( .r ` R ) x )
37 14 36 oveq12i 
 |-  ( ( x ( .r ` O ) y ) ( +g ` R ) ( x ( .r ` O ) z ) ) = ( ( y ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) x ) )
38 34 35 37 3eqtr4g 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( x ( .r ` O ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` O ) y ) ( +g ` R ) ( x ( .r ` O ) z ) ) )
39 2 5 12 ringdi 
 |-  ( ( R e. Ring /\ ( z e. ( Base ` R ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) ) -> ( z ( .r ` R ) ( x ( +g ` R ) y ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) ) )
40 18 19 21 20 39 syl13anc 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( z ( .r ` R ) ( x ( +g ` R ) y ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) ) )
41 2 12 1 13 opprmul 
 |-  ( ( x ( +g ` R ) y ) ( .r ` O ) z ) = ( z ( .r ` R ) ( x ( +g ` R ) y ) )
42 36 28 oveq12i 
 |-  ( ( x ( .r ` O ) z ) ( +g ` R ) ( y ( .r ` O ) z ) ) = ( ( z ( .r ` R ) x ) ( +g ` R ) ( z ( .r ` R ) y ) )
43 40 41 42 3eqtr4g 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( x ( +g ` R ) y ) ( .r ` O ) z ) = ( ( x ( .r ` O ) z ) ( +g ` R ) ( y ( .r ` O ) z ) ) )
44 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
45 2 44 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
46 2 12 1 13 opprmul 
 |-  ( ( 1r ` R ) ( .r ` O ) x ) = ( x ( .r ` R ) ( 1r ` R ) )
47 2 12 44 ringridm 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 1r ` R ) ) = x )
48 46 47 syl5eq 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` O ) x ) = x )
49 2 12 1 13 opprmul 
 |-  ( x ( .r ` O ) ( 1r ` R ) ) = ( ( 1r ` R ) ( .r ` R ) x )
50 2 12 44 ringlidm 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) x ) = x )
51 49 50 syl5eq 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` O ) ( 1r ` R ) ) = x )
52 4 7 8 11 17 32 38 43 45 48 51 isringd 
 |-  ( R e. Ring -> O e. Ring )