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 โŠข ๐ต = ( Base โ€˜ ๐บ )
mulgmhm.m โŠข ยท = ( .g โ€˜ ๐บ )
Assertion mulgghm ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โˆˆ ( ๐บ GrpHom ๐บ ) )

Proof

Step Hyp Ref Expression
1 mulgmhm.b โŠข ๐ต = ( Base โ€˜ ๐บ )
2 mulgmhm.m โŠข ยท = ( .g โ€˜ ๐บ )
3 eqid โŠข ( +g โ€˜ ๐บ ) = ( +g โ€˜ ๐บ )
4 ablgrp โŠข ( ๐บ โˆˆ Abel โ†’ ๐บ โˆˆ Grp )
5 4 adantr โŠข ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ๐บ โˆˆ Grp )
6 1 2 mulgcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ๐‘ฅ ) โˆˆ ๐ต )
7 4 6 syl3an1 โŠข ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ๐‘ฅ ) โˆˆ ๐ต )
8 7 3expa โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘€ ยท ๐‘ฅ ) โˆˆ ๐ต )
9 8 fmpttd โŠข ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) : ๐ต โŸถ ๐ต )
10 3anass โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) โ†” ( ๐‘€ โˆˆ โ„ค โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) )
11 1 2 3 mulgdi โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ( ๐‘€ ยท ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ๐‘€ ยท ๐‘ง ) ) )
12 10 11 sylan2br โŠข ( ( ๐บ โˆˆ Abel โˆง ( ๐‘€ โˆˆ โ„ค โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) ) โ†’ ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ( ๐‘€ ยท ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ๐‘€ ยท ๐‘ง ) ) )
13 12 anassrs โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ( ๐‘€ ยท ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ๐‘€ ยท ๐‘ง ) ) )
14 1 3 grpcl โŠข ( ( ๐บ โˆˆ Grp โˆง ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) โ†’ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) โˆˆ ๐ต )
15 14 3expb โŠข ( ( ๐บ โˆˆ Grp โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) โˆˆ ๐ต )
16 5 15 sylan โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) โˆˆ ๐ต )
17 oveq2 โŠข ( ๐‘ฅ = ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) โ†’ ( ๐‘€ ยท ๐‘ฅ ) = ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) )
18 eqid โŠข ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) = ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) )
19 ovex โŠข ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) โˆˆ V
20 17 18 19 fvmpt โŠข ( ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) โˆˆ ๐ต โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) )
21 16 20 syl โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ๐‘€ ยท ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) )
22 oveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ๐‘€ ยท ๐‘ฅ ) = ( ๐‘€ ยท ๐‘ฆ ) )
23 ovex โŠข ( ๐‘€ ยท ๐‘ฆ ) โˆˆ V
24 22 18 23 fvmpt โŠข ( ๐‘ฆ โˆˆ ๐ต โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ฆ ) = ( ๐‘€ ยท ๐‘ฆ ) )
25 oveq2 โŠข ( ๐‘ฅ = ๐‘ง โ†’ ( ๐‘€ ยท ๐‘ฅ ) = ( ๐‘€ ยท ๐‘ง ) )
26 ovex โŠข ( ๐‘€ ยท ๐‘ง ) โˆˆ V
27 25 18 26 fvmpt โŠข ( ๐‘ง โˆˆ ๐ต โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ง ) = ( ๐‘€ ยท ๐‘ง ) )
28 24 27 oveqan12d โŠข ( ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ง ) ) = ( ( ๐‘€ ยท ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ๐‘€ ยท ๐‘ง ) ) )
29 28 adantl โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ง ) ) = ( ( ๐‘€ ยท ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ๐‘€ ยท ๐‘ง ) ) )
30 13 21 29 3eqtr4d โŠข ( ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โˆง ( ๐‘ฆ โˆˆ ๐ต โˆง ๐‘ง โˆˆ ๐ต ) ) โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ( ๐‘ฆ ( +g โ€˜ ๐บ ) ๐‘ง ) ) = ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ฆ ) ( +g โ€˜ ๐บ ) ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โ€˜ ๐‘ง ) ) )
31 1 1 3 3 5 5 9 30 isghmd โŠข ( ( ๐บ โˆˆ Abel โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ( ๐‘€ ยท ๐‘ฅ ) ) โˆˆ ( ๐บ GrpHom ๐บ ) )