Metamath Proof Explorer


Theorem invghm

Description: The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015)

Ref Expression
Hypotheses invghm.b B = Base G
invghm.m I = inv g G
Assertion invghm G Abel I G GrpHom G

Proof

Step Hyp Ref Expression
1 invghm.b B = Base G
2 invghm.m I = inv g G
3 eqid + G = + G
4 ablgrp G Abel G Grp
5 1 2 grpinvf G Grp I : B B
6 4 5 syl G Abel I : B B
7 1 3 2 ablinvadd G Abel x B y B I x + G y = I x + G I y
8 7 3expb G Abel x B y B I x + G y = I x + G I y
9 1 1 3 3 4 4 6 8 isghmd G Abel I G GrpHom G
10 ghmgrp1 I G GrpHom G G Grp
11 10 adantr I G GrpHom G x B y B G Grp
12 simprr I G GrpHom G x B y B y B
13 simprl I G GrpHom G x B y B x B
14 1 3 2 grpinvadd G Grp y B x B I y + G x = I x + G I y
15 11 12 13 14 syl3anc I G GrpHom G x B y B I y + G x = I x + G I y
16 15 fveq2d I G GrpHom G x B y B I I y + G x = I I x + G I y
17 simpl I G GrpHom G x B y B I G GrpHom G
18 1 2 grpinvcl G Grp x B I x B
19 11 13 18 syl2anc I G GrpHom G x B y B I x B
20 1 2 grpinvcl G Grp y B I y B
21 11 12 20 syl2anc I G GrpHom G x B y B I y B
22 1 3 3 ghmlin I G GrpHom G I x B I y B I I x + G I y = I I x + G I I y
23 17 19 21 22 syl3anc I G GrpHom G x B y B I I x + G I y = I I x + G I I y
24 1 2 grpinvinv G Grp x B I I x = x
25 11 13 24 syl2anc I G GrpHom G x B y B I I x = x
26 1 2 grpinvinv G Grp y B I I y = y
27 11 12 26 syl2anc I G GrpHom G x B y B I I y = y
28 25 27 oveq12d I G GrpHom G x B y B I I x + G I I y = x + G y
29 16 23 28 3eqtrd I G GrpHom G x B y B I I y + G x = x + G y
30 1 3 grpcl G Grp y B x B y + G x B
31 11 12 13 30 syl3anc I G GrpHom G x B y B y + G x B
32 1 2 grpinvinv G Grp y + G x B I I y + G x = y + G x
33 11 31 32 syl2anc I G GrpHom G x B y B I I y + G x = y + G x
34 29 33 eqtr3d I G GrpHom G x B y B x + G y = y + G x
35 34 ralrimivva I G GrpHom G x B y B x + G y = y + G x
36 1 3 isabl2 G Abel G Grp x B y B x + G y = y + G x
37 10 35 36 sylanbrc I G GrpHom G G Abel
38 9 37 impbii G Abel I G GrpHom G