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

Metamath Proof Explorer

Theorem oppginv

Description: Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypotheses oppgbas.1 
|- O = ( oppG ` R )
oppginv.2 
|- I = ( invg ` R )
Assertion oppginv 
|- ( R e. Grp -> I = ( invg ` O ) )

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 oppginv.2 
 |-  I = ( invg ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 3 2 grpinvf 
 |-  ( R e. Grp -> I : ( Base ` R ) --> ( Base ` R ) )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 eqid 
 |-  ( +g ` O ) = ( +g ` O )
7 5 1 6 oppgplus 
 |-  ( ( I ` x ) ( +g ` O ) x ) = ( x ( +g ` R ) ( I ` x ) )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 3 5 8 2 grprinv 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( x ( +g ` R ) ( I ` x ) ) = ( 0g ` R ) )
10 7 9 eqtrid 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( ( I ` x ) ( +g ` O ) x ) = ( 0g ` R ) )
11 10 ralrimiva 
 |-  ( R e. Grp -> A. x e. ( Base ` R ) ( ( I ` x ) ( +g ` O ) x ) = ( 0g ` R ) )
12 1 oppggrp 
 |-  ( R e. Grp -> O e. Grp )
13 1 3 oppgbas 
 |-  ( Base ` R ) = ( Base ` O )
14 1 8 oppgid 
 |-  ( 0g ` R ) = ( 0g ` O )
15 eqid 
 |-  ( invg ` O ) = ( invg ` O )
16 13 6 14 15 isgrpinv 
 |-  ( O e. Grp -> ( ( I : ( Base ` R ) --> ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( I ` x ) ( +g ` O ) x ) = ( 0g ` R ) ) <-> ( invg ` O ) = I ) )
17 12 16 syl 
 |-  ( R e. Grp -> ( ( I : ( Base ` R ) --> ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( I ` x ) ( +g ` O ) x ) = ( 0g ` R ) ) <-> ( invg ` O ) = I ) )
18 4 11 17 mpbi2and 
 |-  ( R e. Grp -> ( invg ` O ) = I )
19 18 eqcomd 
 |-  ( R e. Grp -> I = ( invg ` O ) )