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