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 
|- .x. = ( .g ` G )
Assertion mulgghm 
|- ( ( G e. Abel /\ M e. ZZ ) -> ( x e. B |-> ( M .x. x ) ) e. ( G GrpHom G ) )

Proof

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