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 \in Abel \leftrightarrow I \in (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 \in Abel \to G \in Grp$
5	1 2	grpinvf	$⊢ G \in Grp \to I : B ⟶ B$
6	4 5	syl	$⊢ G \in Abel \to I : B ⟶ B$
7	1 3 2	ablinvadd	$⊢ (G \in Abel \land x \in B \land y \in B) \to I (x +_{G} y) = I (x) +_{G} I (y)$
8	7	3expb	$⊢ (G \in Abel \land (x \in B \land y \in B)) \to I (x +_{G} y) = I (x) +_{G} I (y)$
9	1 1 3 3 4 4 6 8	isghmd	$⊢ G \in Abel \to I \in (G GrpHom G)$
10		ghmgrp1	$⊢ I \in (G GrpHom G) \to G \in Grp$
11	10	adantr	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to G \in Grp$
12		simprr	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to y \in B$
13		simprl	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to x \in B$
14	1 3 2	grpinvadd	$⊢ (G \in Grp \land y \in B \land x \in B) \to I (y +_{G} x) = I (x) +_{G} I (y)$
15	11 12 13 14	syl3anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (y +_{G} x) = I (x) +_{G} I (y)$
16	15	fveq2d	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (y +_{G} x)) = I (I (x) +_{G} I (y))$
17		simpl	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I \in (G GrpHom G)$
18	1 2	grpinvcl	$⊢ (G \in Grp \land x \in B) \to I (x) \in B$
19	11 13 18	syl2anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (x) \in B$
20	1 2	grpinvcl	$⊢ (G \in Grp \land y \in B) \to I (y) \in B$
21	11 12 20	syl2anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (y) \in B$
22	1 3 3	ghmlin	$⊢ (I \in (G GrpHom G) \land I (x) \in B \land I (y) \in B) \to I (I (x) +_{G} I (y)) = I (I (x)) +_{G} I (I (y))$
23	17 19 21 22	syl3anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (x) +_{G} I (y)) = I (I (x)) +_{G} I (I (y))$
24	1 2	grpinvinv	$⊢ (G \in Grp \land x \in B) \to I (I (x)) = x$
25	11 13 24	syl2anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (x)) = x$
26	1 2	grpinvinv	$⊢ (G \in Grp \land y \in B) \to I (I (y)) = y$
27	11 12 26	syl2anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (y)) = y$
28	25 27	oveq12d	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (x)) +_{G} I (I (y)) = x +_{G} y$
29	16 23 28	3eqtrd	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (y +_{G} x)) = x +_{G} y$
30	1 3	grpcl	$⊢ (G \in Grp \land y \in B \land x \in B) \to y +_{G} x \in B$
31	11 12 13 30	syl3anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to y +_{G} x \in B$
32	1 2	grpinvinv	$⊢ (G \in Grp \land y +_{G} x \in B) \to I (I (y +_{G} x)) = y +_{G} x$
33	11 31 32	syl2anc	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to I (I (y +_{G} x)) = y +_{G} x$
34	29 33	eqtr3d	$⊢ (I \in (G GrpHom G) \land (x \in B \land y \in B)) \to x +_{G} y = y +_{G} x$
35	34	ralrimivva	$⊢ I \in (G GrpHom G) \to \forall x \in B \forall y \in B x +_{G} y = y +_{G} x$
36	1 3	isabl2	$⊢ G \in Abel \leftrightarrow (G \in Grp \land \forall x \in B \forall y \in B x +_{G} y = y +_{G} x)$
37	10 35 36	sylanbrc	$⊢ I \in (G GrpHom G) \to G \in Abel$
38	9 37	impbii	$⊢ G \in Abel \leftrightarrow I \in (G GrpHom G)$

Metamath Proof Explorer

Theorem invghm

Proof