Metamath Proof Explorer


Theorem mulgmhm

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

Ref Expression
Hypotheses mulgmhm.b B = Base G
mulgmhm.m · ˙ = G
Assertion mulgmhm G CMnd M 0 x B M · ˙ x G MndHom G

Proof

Step Hyp Ref Expression
1 mulgmhm.b B = Base G
2 mulgmhm.m · ˙ = G
3 cmnmnd G CMnd G Mnd
4 3 adantr G CMnd M 0 G Mnd
5 1 2 mulgnn0cl G Mnd M 0 x B M · ˙ x B
6 3 5 syl3an1 G CMnd M 0 x B M · ˙ x B
7 6 3expa G CMnd M 0 x B M · ˙ x B
8 7 fmpttd G CMnd M 0 x B M · ˙ x : B B
9 3anass M 0 y B z B M 0 y B z B
10 eqid + G = + G
11 1 2 10 mulgnn0di G CMnd M 0 y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
12 9 11 sylan2br G CMnd M 0 y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
13 12 anassrs G CMnd M 0 y B z B M · ˙ y + G z = M · ˙ y + G M · ˙ z
14 1 10 mndcl G Mnd y B z B y + G z B
15 14 3expb G Mnd y B z B y + G z B
16 4 15 sylan G CMnd M 0 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 CMnd M 0 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 CMnd M 0 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 CMnd M 0 y B z B x B M · ˙ x y + G z = x B M · ˙ x y + G x B M · ˙ x z
31 30 ralrimivva G CMnd M 0 y B z B x B M · ˙ x y + G z = x B M · ˙ x y + G x B M · ˙ x z
32 eqid 0 G = 0 G
33 1 32 mndidcl G Mnd 0 G B
34 oveq2 x = 0 G M · ˙ x = M · ˙ 0 G
35 ovex M · ˙ 0 G V
36 34 18 35 fvmpt 0 G B x B M · ˙ x 0 G = M · ˙ 0 G
37 4 33 36 3syl G CMnd M 0 x B M · ˙ x 0 G = M · ˙ 0 G
38 1 2 32 mulgnn0z G Mnd M 0 M · ˙ 0 G = 0 G
39 3 38 sylan G CMnd M 0 M · ˙ 0 G = 0 G
40 37 39 eqtrd G CMnd M 0 x B M · ˙ x 0 G = 0 G
41 8 31 40 3jca G CMnd M 0 x B M · ˙ x : B B y B z B x B M · ˙ x y + G z = x B M · ˙ x y + G x B M · ˙ x z x B M · ˙ x 0 G = 0 G
42 1 1 10 10 32 32 ismhm x B M · ˙ x G MndHom G G Mnd G Mnd x B M · ˙ x : B B y B z B x B M · ˙ x y + G z = x B M · ˙ x y + G x B M · ˙ x z x B M · ˙ x 0 G = 0 G
43 4 4 41 42 syl21anbrc G CMnd M 0 x B M · ˙ x G MndHom G