Metamath Proof Explorer


Theorem mulgghm

Description: The map from x to n x for a fixed integer n is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015)

Ref Expression
Hypotheses mulgmhm.b B = Base G
mulgmhm.m · ˙ = G
Assertion mulgghm G Abel M x B M · ˙ x G GrpHom G

Proof

Step Hyp Ref Expression
1 mulgmhm.b B = Base G
2 mulgmhm.m · ˙ = G
3 eqid + G = + G
4 ablgrp G Abel G Grp
5 4 adantr G Abel M G Grp
6 1 2 mulgcl G Grp M x B M · ˙ x B
7 4 6 syl3an1 G Abel M x B M · ˙ x B
8 7 3expa G Abel M x B M · ˙ x B
9 8 fmpttd G Abel M x B M · ˙ x : B B
10 3anass M y B z B M y B z B
11 1 2 3 mulgdi G Abel M y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
12 10 11 sylan2br G Abel M y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
13 12 anassrs G Abel M y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
14 1 3 grpcl G Grp y B z B y + G z B
15 14 3expb G Grp y B z B y + G z B
16 5 15 sylan G Abel M y B z B y + G z B
17 oveq2 x = y + G z M · ˙ x = M · ˙ y + G z
18 eqid x B M · ˙ x = x B M · ˙ x
19 ovex M · ˙ y + G z V
20 17 18 19 fvmpt y + G z B x B M · ˙ x y + G z = M · ˙ y + G z
21 16 20 syl G Abel M y B z B x B M · ˙ x y + G z = M · ˙ y + G z
22 oveq2 x = y M · ˙ x = M · ˙ y
23 ovex M · ˙ y V
24 22 18 23 fvmpt y B x B M · ˙ x y = M · ˙ y
25 oveq2 x = z M · ˙ x = M · ˙ z
26 ovex M · ˙ z V
27 25 18 26 fvmpt z B x B M · ˙ x z = M · ˙ z
28 24 27 oveqan12d y B z B x B M · ˙ x y + G x B M · ˙ x z = M · ˙ y + G M · ˙ z
29 28 adantl G Abel M y B z B x B M · ˙ x y + G x B M · ˙ x z = M · ˙ y + G M · ˙ z
30 13 21 29 3eqtr4d G Abel M y B z B x B M · ˙ x y + G z = x B M · ˙ x y + G x B M · ˙ x z
31 1 1 3 3 5 5 9 30 isghmd G Abel M x B M · ˙ x G GrpHom G