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

Metamath Proof Explorer

Theorem oppggrp

Description: The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015)

Ref Expression
Hypothesis oppgbas.1 
|- O = ( oppG ` R )
Assertion oppggrp 
|- ( R e. Grp -> O e. Grp )

Proof

Step Hyp Ref Expression
1 oppgbas.1 
 |-  O = ( oppG ` R )
2 eqid 
 |-  ( Base ` R ) = ( Base ` R )
3 1 2 oppgbas 
 |-  ( Base ` R ) = ( Base ` O )
4 3 a1i 
 |-  ( R e. Grp -> ( Base ` R ) = ( Base ` O ) )
5 eqidd 
 |-  ( R e. Grp -> ( +g ` O ) = ( +g ` O ) )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 1 6 oppgid 
 |-  ( 0g ` R ) = ( 0g ` O )
8 7 a1i 
 |-  ( R e. Grp -> ( 0g ` R ) = ( 0g ` O ) )
9 grpmnd 
 |-  ( R e. Grp -> R e. Mnd )
10 1 oppgmnd 
 |-  ( R e. Mnd -> O e. Mnd )
11 9 10 syl 
 |-  ( R e. Grp -> O e. Mnd )
12 eqid 
 |-  ( invg ` R ) = ( invg ` R )
13 2 12 grpinvcl 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( ( invg ` R ) ` x ) e. ( Base ` R ) )
14 eqid 
 |-  ( +g ` R ) = ( +g ` R )
15 eqid 
 |-  ( +g ` O ) = ( +g ` O )
16 14 1 15 oppgplus 
 |-  ( ( ( invg ` R ) ` x ) ( +g ` O ) x ) = ( x ( +g ` R ) ( ( invg ` R ) ` x ) )
17 2 14 6 12 grprinv 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( x ( +g ` R ) ( ( invg ` R ) ` x ) ) = ( 0g ` R ) )
18 16 17 eqtrid 
 |-  ( ( R e. Grp /\ x e. ( Base ` R ) ) -> ( ( ( invg ` R ) ` x ) ( +g ` O ) x ) = ( 0g ` R ) )
19 4 5 8 11 13 18 isgrpd2 
 |-  ( R e. Grp -> O e. Grp )