Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulgghm Structured version   Unicode version

Theorem mulgghm 17161
 Description: The map from to for a fixed integer is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.)
Hypotheses
Ref Expression
mulgmhm.b
mulgmhm.m .g
Assertion
Ref Expression
mulgghm
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem mulgghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mulgmhm.b . 2
2 eqid 2402 . 2
3 ablgrp 17127 . . 3
5 mulgmhm.m . . . . . 6 .g
61, 5mulgcl 16483 . . . . 5
73, 6syl3an1 1263 . . . 4
873expa 1197 . . 3
9 eqid 2402 . . 3
108, 9fmptd 6033 . 2
11 3anass 978 . . . . 5
121, 5, 2mulgdi 17159 . . . . 5
1311, 12sylan2br 474 . . . 4
1413anassrs 646 . . 3
151, 2grpcl 16387 . . . . . 6
16153expb 1198 . . . . 5
174, 16sylan 469 . . . 4
18 oveq2 6286 . . . . 5
19 ovex 6306 . . . . 5
2018, 9, 19fvmpt 5932 . . . 4
2117, 20syl 17 . . 3
22 oveq2 6286 . . . . . 6
23 ovex 6306 . . . . . 6
2422, 9, 23fvmpt 5932 . . . . 5
25 oveq2 6286 . . . . . 6
26 ovex 6306 . . . . . 6
2725, 9, 26fvmpt 5932 . . . . 5
2824, 27oveqan12d 6297 . . . 4