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