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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgghm	$⊢ (G \in Abel \land M \in ℤ) \to (x \in B ⟼ M \underset{˙}{\cdot} x) \in (G GrpHom G)$

Proof

Step	Hyp	Ref	Expression
1		mulgmhm.b	$⊢ B = {Base}_{G}$
2		mulgmhm.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		eqid	$⊢ +_{G} = +_{G}$
4		ablgrp	$⊢ G \in Abel \to G \in Grp$
5	4	adantr	$⊢ (G \in Abel \land M \in ℤ) \to G \in Grp$
6	1 2	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land x \in B) \to M \underset{˙}{\cdot} x \in B$
7	4 6	syl3an1	$⊢ (G \in Abel \land M \in ℤ \land x \in B) \to M \underset{˙}{\cdot} x \in B$
8	7	3expa	$⊢ ((G \in Abel \land M \in ℤ) \land x \in B) \to M \underset{˙}{\cdot} x \in B$
9	8	fmpttd	$⊢ (G \in Abel \land M \in ℤ) \to (x \in B ⟼ M \underset{˙}{\cdot} x) : B ⟶ B$
10		3anass	$⊢ (M \in ℤ \land y \in B \land z \in B) \leftrightarrow (M \in ℤ \land (y \in B \land z \in B))$
11	1 2 3	mulgdi	$⊢ (G \in Abel \land (M \in ℤ \land y \in B \land z \in B)) \to M \underset{˙}{\cdot} (y +_{G} z) = (M \underset{˙}{\cdot} y) +_{G} (M \underset{˙}{\cdot} z)$
12	10 11	sylan2br	$⊢ (G \in Abel \land (M \in ℤ \land (y \in B \land z \in B))) \to M \underset{˙}{\cdot} (y +_{G} z) = (M \underset{˙}{\cdot} y) +_{G} (M \underset{˙}{\cdot} z)$
13	12	anassrs	$⊢ ((G \in Abel \land M \in ℤ) \land (y \in B \land z \in B)) \to M \underset{˙}{\cdot} (y +_{G} z) = (M \underset{˙}{\cdot} y) +_{G} (M \underset{˙}{\cdot} z)$
14	1 3	grpcl	$⊢ (G \in Grp \land y \in B \land z \in B) \to y +_{G} z \in B$
15	14	3expb	$⊢ (G \in Grp \land (y \in B \land z \in B)) \to y +_{G} z \in B$
16	5 15	sylan	$⊢ ((G \in Abel \land M \in ℤ) \land (y \in B \land z \in B)) \to y +_{G} z \in B$
17		oveq2	$⊢ x = y +_{G} z \to M \underset{˙}{\cdot} x = M \underset{˙}{\cdot} (y +_{G} z)$
18		eqid	$⊢ (x \in B ⟼ M \underset{˙}{\cdot} x) = (x \in B ⟼ M \underset{˙}{\cdot} x)$
19		ovex	$⊢ M \underset{˙}{\cdot} (y +_{G} z) \in V$
20	17 18 19	fvmpt	$⊢ y +_{G} z \in B \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y +_{G} z) = M \underset{˙}{\cdot} (y +_{G} z)$
21	16 20	syl	$⊢ ((G \in Abel \land M \in ℤ) \land (y \in B \land z \in B)) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y +_{G} z) = M \underset{˙}{\cdot} (y +_{G} z)$
22		oveq2	$⊢ x = y \to M \underset{˙}{\cdot} x = M \underset{˙}{\cdot} y$
23		ovex	$⊢ M \underset{˙}{\cdot} y \in V$
24	22 18 23	fvmpt	$⊢ y \in B \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y) = M \underset{˙}{\cdot} y$
25		oveq2	$⊢ x = z \to M \underset{˙}{\cdot} x = M \underset{˙}{\cdot} z$
26		ovex	$⊢ M \underset{˙}{\cdot} z \in V$
27	25 18 26	fvmpt	$⊢ z \in B \to (x \in B ⟼ M \underset{˙}{\cdot} x) (z) = M \underset{˙}{\cdot} z$
28	24 27	oveqan12d	$⊢ (y \in B \land z \in B) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y) +_{G} (x \in B ⟼ M \underset{˙}{\cdot} x) (z) = (M \underset{˙}{\cdot} y) +_{G} (M \underset{˙}{\cdot} z)$
29	28	adantl	$⊢ ((G \in Abel \land M \in ℤ) \land (y \in B \land z \in B)) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y) +_{G} (x \in B ⟼ M \underset{˙}{\cdot} x) (z) = (M \underset{˙}{\cdot} y) +_{G} (M \underset{˙}{\cdot} z)$
30	13 21 29	3eqtr4d	$⊢ ((G \in Abel \land M \in ℤ) \land (y \in B \land z \in B)) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (y +_{G} z) = (x \in B ⟼ M \underset{˙}{\cdot} x) (y) +_{G} (x \in B ⟼ M \underset{˙}{\cdot} x) (z)$
31	1 1 3 3 5 5 9 30	isghmd	$⊢ (G \in Abel \land M \in ℤ) \to (x \in B ⟼ M \underset{˙}{\cdot} x) \in (G GrpHom G)$

Metamath Proof Explorer

Theorem mulgghm

Proof