Metamath Proof Explorer

Theorem invoppggim

Description: The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypotheses invoppggim.o 
|- O = ( oppG ` G )
invoppggim.i 
|- I = ( invg ` G )
Assertion invoppggim 
|- ( G e. Grp -> I e. ( G GrpIso O ) )

Proof

Step Hyp Ref Expression
1 invoppggim.o 
 |-  O = ( oppG ` G )
2 invoppggim.i 
 |-  I = ( invg ` G )
3 eqid 
 |-  ( Base ` G ) = ( Base ` G )
4 1 3 oppgbas 
 |-  ( Base ` G ) = ( Base ` O )
5 eqid 
 |-  ( +g ` G ) = ( +g ` G )
6 eqid 
 |-  ( +g ` O ) = ( +g ` O )
7 id 
 |-  ( G e. Grp -> G e. Grp )
8 1 oppggrp 
 |-  ( G e. Grp -> O e. Grp )
9 3 2 grpinvf 
 |-  ( G e. Grp -> I : ( Base ` G ) --> ( Base ` G ) )
10 3 5 2 grpinvadd 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( I ` ( x ( +g ` G ) y ) ) = ( ( I ` y ) ( +g ` G ) ( I ` x ) ) )
11 10 3expb 
 |-  ( ( G e. Grp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( I ` ( x ( +g ` G ) y ) ) = ( ( I ` y ) ( +g ` G ) ( I ` x ) ) )
12 5 1 6 oppgplus 
 |-  ( ( I ` x ) ( +g ` O ) ( I ` y ) ) = ( ( I ` y ) ( +g ` G ) ( I ` x ) )
13 11 12 eqtr4di 
 |-  ( ( G e. Grp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( I ` ( x ( +g ` G ) y ) ) = ( ( I ` x ) ( +g ` O ) ( I ` y ) ) )
14 3 4 5 6 7 8 9 13 isghmd 
 |-  ( G e. Grp -> I e. ( G GrpHom O ) )
15 3 2 7 grpinvf1o 
 |-  ( G e. Grp -> I : ( Base ` G ) -1-1-onto-> ( Base ` G ) )
16 3 4 isgim 
 |-  ( I e. ( G GrpIso O ) <-> ( I e. ( G GrpHom O ) /\ I : ( Base ` G ) -1-1-onto-> ( Base ` G ) ) )
17 14 15 16 sylanbrc 
 |-  ( G e. Grp -> I e. ( G GrpIso O ) )