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

Metamath Proof Explorer

Theorem grpinvcnv

Description: The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Hypotheses grpinvinv.b 
|- B = ( Base ` G )
grpinvinv.n 
|- N = ( invg ` G )
Assertion grpinvcnv 
|- ( G e. Grp -> `' N = N )

Proof

Step Hyp Ref Expression
1 grpinvinv.b 
 |-  B = ( Base ` G )
2 grpinvinv.n 
 |-  N = ( invg ` G )
3 eqid 
 |-  ( x e. B |-> ( N ` x ) ) = ( x e. B |-> ( N ` x ) )
4 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ x e. B ) -> ( N ` x ) e. B )
5 1 2 grpinvcl 
 |-  ( ( G e. Grp /\ y e. B ) -> ( N ` y ) e. B )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
8 1 6 7 2 grpinvid1 
 |-  ( ( G e. Grp /\ y e. B /\ x e. B ) -> ( ( N ` y ) = x <-> ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
9 8 3com23 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( ( N ` y ) = x <-> ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
10 1 6 7 2 grpinvid2 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( ( N ` x ) = y <-> ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
11 9 10 bitr4d 
 |-  ( ( G e. Grp /\ x e. B /\ y e. B ) -> ( ( N ` y ) = x <-> ( N ` x ) = y ) )
12 11 3expb 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( ( N ` y ) = x <-> ( N ` x ) = y ) )
13 eqcom 
 |-  ( x = ( N ` y ) <-> ( N ` y ) = x )
14 eqcom 
 |-  ( y = ( N ` x ) <-> ( N ` x ) = y )
15 12 13 14 3bitr4g 
 |-  ( ( G e. Grp /\ ( x e. B /\ y e. B ) ) -> ( x = ( N ` y ) <-> y = ( N ` x ) ) )
16 3 4 5 15 f1ocnv2d 
 |-  ( G e. Grp -> ( ( x e. B |-> ( N ` x ) ) : B -1-1-onto-> B /\ `' ( x e. B |-> ( N ` x ) ) = ( y e. B |-> ( N ` y ) ) ) )
17 16 simprd 
 |-  ( G e. Grp -> `' ( x e. B |-> ( N ` x ) ) = ( y e. B |-> ( N ` y ) ) )
18 1 2 grpinvf 
 |-  ( G e. Grp -> N : B --> B )
19 18 feqmptd 
 |-  ( G e. Grp -> N = ( x e. B |-> ( N ` x ) ) )
20 19 cnveqd 
 |-  ( G e. Grp -> `' N = `' ( x e. B |-> ( N ` x ) ) )
21 18 feqmptd 
 |-  ( G e. Grp -> N = ( y e. B |-> ( N ` y ) ) )
22 17 20 21 3eqtr4d 
 |-  ( G e. Grp -> `' N = N )