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
|- .x. = ( .g ` G )
Assertion mulgmhm
|- ( ( G e. CMnd /\ M e. NN0 ) -> ( x e. B |-> ( M .x. x ) ) e. ( G MndHom G ) )

Proof

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