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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
invghm.m ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion invghm ( 𝐺 ∈ Abel ↔ 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )

Proof

Step Hyp Ref Expression
1 invghm.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 invghm.m ⊢ 𝐼 = ( invg ‘ 𝐺 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
5 1 2 grpinvf ⊢ ( 𝐺 ∈ Grp → 𝐼 : 𝐵 ⟶ 𝐵 )
6 4 5 syl ⊢ ( 𝐺 ∈ Abel → 𝐼 : 𝐵 ⟶ 𝐵 )
7 1 3 2 ablinvadd ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) )
8 7 3expb ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) )
9 1 1 3 3 4 4 6 8 isghmd ⊢ ( 𝐺 ∈ Abel → 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
10 ghmgrp1 ⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐺 ∈ Grp )
11 10 adantr ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
12 simprr ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
13 simprl ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
14 1 3 2 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) )
15 11 12 13 14 syl3anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) = ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) )
16 15 fveq2d ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝐼 ‘ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) ) )
17 simpl ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
18 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐵 )
19 11 13 18 syl2anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐵 )
20 1 2 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝐵 )
21 11 12 20 syl2anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝐵 )
22 1 3 3 ghmlin ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) ) = ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑥 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ ( 𝐼 ‘ 𝑦 ) ) ) )
23 17 19 21 22 syl3anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( ( 𝐼 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑦 ) ) ) = ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑥 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ ( 𝐼 ‘ 𝑦 ) ) ) )
24 1 2 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑥 ) ) = 𝑥 )
25 11 13 24 syl2anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑥 ) ) = 𝑥 )
26 1 2 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑦 ) ) = 𝑦 )
27 11 12 26 syl2anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑦 ) ) = 𝑦 )
28 25 27 oveq12d ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑥 ) ) ( +g ‘ 𝐺 ) ( 𝐼 ‘ ( 𝐼 ‘ 𝑦 ) ) ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
29 16 23 28 3eqtrd ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
30 1 3 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
31 11 12 13 30 syl3anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 )
32 1 2 grpinvinv ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
33 11 31 32 syl2anc ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
34 29 33 eqtr3d ⊢ ( ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
35 34 ralrimivva ⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) )
36 1 3 isabl2 ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) ) )
37 10 35 36 sylanbrc ⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐺 ∈ Abel )
38 9 37 impbii ⊢ ( 𝐺 ∈ Abel ↔ 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )