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

Metamath Proof Explorer

Theorem opprneg

Description: The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opprbas.1 
|- O = ( oppR ` R )
opprneg.2 
|- N = ( invg ` R )
Assertion opprneg 
|- N = ( invg ` O )

Proof

Step Hyp Ref Expression
1 opprbas.1 
 |-  O = ( oppR ` R )
2 opprneg.2 
 |-  N = ( invg ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( +g ` R ) = ( +g ` R )
5 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
6 3 4 5 2 grpinvfval 
 |-  N = ( x e. ( Base ` R ) |-> ( iota_ y e. ( Base ` R ) ( y ( +g ` R ) x ) = ( 0g ` R ) ) )
7 1 3 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
8 1 4 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
9 1 5 oppr0 
 |-  ( 0g ` R ) = ( 0g ` O )
10 eqid 
 |-  ( invg ` O ) = ( invg ` O )
11 7 8 9 10 grpinvfval 
 |-  ( invg ` O ) = ( x e. ( Base ` R ) |-> ( iota_ y e. ( Base ` R ) ( y ( +g ` R ) x ) = ( 0g ` R ) ) )
12 6 11 eqtr4i 
 |-  N = ( invg ` O )