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

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 = ( invg ` G )
Assertion invghm 
|- ( G e. Abel <-> I e. ( G GrpHom G ) )

Proof

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