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

Metamath Proof Explorer

Theorem opprrng

Description: An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025)

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

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. Rng -> ( Base ` R ) = ( Base ` O ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 1 5 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
7 6 a1i 
 |-  ( R e. Rng -> ( +g ` R ) = ( +g ` O ) )
8 eqidd 
 |-  ( R e. Rng -> ( .r ` O ) = ( .r ` O ) )
9 rngabl 
 |-  ( R e. Rng -> R e. Abel )
10 3 6 ablprop 
 |-  ( R e. Abel <-> O e. Abel )
11 9 10 sylib 
 |-  ( R e. Rng -> O e. Abel )
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 rngcl 
 |-  ( ( R e. Rng /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( y ( .r ` R ) x ) e. ( Base ` R ) )
16 15 3com23 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( y ( .r ` R ) x ) e. ( Base ` R ) )
17 14 16 eqeltrid 
 |-  ( ( R e. Rng /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( x ( .r ` O ) y ) e. ( Base ` R ) )
18 simpl 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> R e. Rng )
19 simpr3 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> z e. ( Base ` R ) )
20 simpr2 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> y e. ( Base ` R ) )
21 simpr1 
 |-  ( ( R e. Rng /\ ( x e. ( Base ` R ) /\ y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> x e. ( Base ` R ) )
22 2 12 rngass 
 |-  ( ( R e. Rng /\ ( 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. Rng /\ ( 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. Rng /\ ( 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. Rng /\ ( 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 rngdir 
 |-  ( ( R e. Rng /\ ( 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. Rng /\ ( 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. Rng /\ ( 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 rngdi 
 |-  ( ( R e. Rng /\ ( 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. Rng /\ ( 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. Rng /\ ( 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 4 7 8 11 17 32 38 43 isrngd 
 |-  ( R e. Rng -> O e. Rng )