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 = inv g G
Assertion grpinvcnv G Grp N -1 = N

Proof

Step Hyp Ref Expression
1 grpinvinv.b B = Base G
2 grpinvinv.n N = inv g G
3 eqid x B N x = x B N x
4 1 2 grpinvcl G Grp x B N x B
5 1 2 grpinvcl G Grp y B N y B
6 eqid + G = + G
7 eqid 0 G = 0 G
8 1 6 7 2 grpinvid1 G Grp y B x B N y = x y + G x = 0 G
9 8 3com23 G Grp x B y B N y = x y + G x = 0 G
10 1 6 7 2 grpinvid2 G Grp x B y B N x = y y + G x = 0 G
11 9 10 bitr4d G Grp x B y B N y = x N x = y
12 11 3expb G Grp x B y 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 Grp x B y B x = N y y = N x
16 3 4 5 15 f1ocnv2d G Grp x B N x : B 1-1 onto B x B N x -1 = y B N y
17 16 simprd G Grp x B N x -1 = y B N y
18 1 2 grpinvf G Grp N : B B
19 18 feqmptd G Grp N = x B N x
20 19 cnveqd G Grp N -1 = x B N x -1
21 18 feqmptd G Grp N = y B N y
22 17 20 21 3eqtr4d G Grp N -1 = N