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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	mulgmhm	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to (x \in B ⟼ M \underset{˙}{\cdot} x) \in (G MndHom G)$

Proof

Step	Hyp	Ref	Expression
1		mulgmhm.b	$⊢ B = {Base}_{G}$
2		mulgmhm.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
4	3	adantr	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to G \in Mnd$
5	1 2	mulgnn0cl	$⊢ (G \in Mnd \land M \in ℕ_{0} \land x \in B) \to M \underset{˙}{\cdot} x \in B$
6	3 5	syl3an1	$⊢ (G \in CMnd \land M \in ℕ_{0} \land x \in B) \to M \underset{˙}{\cdot} x \in B$
7	6	3expa	$⊢ ((G \in CMnd \land M \in ℕ_{0}) \land x \in B) \to M \underset{˙}{\cdot} x \in B$
8	7	fmpttd	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to (x \in B ⟼ M \underset{˙}{\cdot} x) : B ⟶ B$
9		3anass	$⊢ (M \in ℕ_{0} \land y \in B \land z \in B) \leftrightarrow (M \in ℕ_{0} \land (y \in B \land z \in B))$
10		eqid	$⊢ +_{G} = +_{G}$
11	1 2 10	mulgnn0di	$⊢ (G \in CMnd \land (M \in ℕ_{0} \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	9 11	sylan2br	$⊢ (G \in CMnd \land (M \in ℕ_{0} \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 CMnd \land M \in ℕ_{0}) \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 10	mndcl	$⊢ (G \in Mnd \land y \in B \land z \in B) \to y +_{G} z \in B$
15	14	3expb	$⊢ (G \in Mnd \land (y \in B \land z \in B)) \to y +_{G} z \in B$
16	4 15	sylan	$⊢ ((G \in CMnd \land M \in ℕ_{0}) \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 CMnd \land M \in ℕ_{0}) \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 CMnd \land M \in ℕ_{0}) \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 CMnd \land M \in ℕ_{0}) \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	30	ralrimivva	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to \forall y \in B \forall z \in B (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)$
32		eqid	$⊢ 0_{G} = 0_{G}$
33	1 32	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
34		oveq2	$⊢ x = 0_{G} \to M \underset{˙}{\cdot} x = M \underset{˙}{\cdot} 0_{G}$
35		ovex	$⊢ M \underset{˙}{\cdot} 0_{G} \in V$
36	34 18 35	fvmpt	$⊢ 0_{G} \in B \to (x \in B ⟼ M \underset{˙}{\cdot} x) (0_{G}) = M \underset{˙}{\cdot} 0_{G}$
37	4 33 36	3syl	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (0_{G}) = M \underset{˙}{\cdot} 0_{G}$
38	1 2 32	mulgnn0z	$⊢ (G \in Mnd \land M \in ℕ_{0}) \to M \underset{˙}{\cdot} 0_{G} = 0_{G}$
39	3 38	sylan	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to M \underset{˙}{\cdot} 0_{G} = 0_{G}$
40	37 39	eqtrd	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to (x \in B ⟼ M \underset{˙}{\cdot} x) (0_{G}) = 0_{G}$
41	8 31 40	3jca	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to ((x \in B ⟼ M \underset{˙}{\cdot} x) : B ⟶ B \land \forall y \in B \forall z \in B (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) \land (x \in B ⟼ M \underset{˙}{\cdot} x) (0_{G}) = 0_{G})$
42	1 1 10 10 32 32	ismhm	$⊢ (x \in B ⟼ M \underset{˙}{\cdot} x) \in (G MndHom G) \leftrightarrow ((G \in Mnd \land G \in Mnd) \land ((x \in B ⟼ M \underset{˙}{\cdot} x) : B ⟶ B \land \forall y \in B \forall z \in B (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) \land (x \in B ⟼ M \underset{˙}{\cdot} x) (0_{G}) = 0_{G}))$
43	4 4 41 42	syl21anbrc	$⊢ (G \in CMnd \land M \in ℕ_{0}) \to (x \in B ⟼ M \underset{˙}{\cdot} x) \in (G MndHom G)$

Metamath Proof Explorer

Theorem mulgmhm

Proof