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 syl5eq
 |-  ( ( 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 ) )