This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )