mulgghm2

Description: The powers of a group element give a homomorphism from ZZ to a group. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypotheses	mulgghm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mulgghm2.f	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
	mulgghm2.b	$⊢ B = {Base}_{R}$
Assertion	mulgghm2	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to F \in (ℤ_{ring} GrpHom R)$

Proof

Step	Hyp	Ref	Expression
1		mulgghm2.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		mulgghm2.f	$⊢ F = (n \in ℤ ⟼ n \underset{˙}{\cdot} \underset{˙}{1})$
3		mulgghm2.b	$⊢ B = {Base}_{R}$
4		simpl	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to R \in Grp$
5		zringgrp	$⊢ ℤ_{ring} \in Grp$
6	4 5	jctil	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to (ℤ_{ring} \in Grp \land R \in Grp)$
7	3 1	mulgcl	$⊢ (R \in Grp \land n \in ℤ \land \underset{˙}{1} \in B) \to n \underset{˙}{\cdot} \underset{˙}{1} \in B$
8	7	3expa	$⊢ ((R \in Grp \land n \in ℤ) \land \underset{˙}{1} \in B) \to n \underset{˙}{\cdot} \underset{˙}{1} \in B$
9	8	an32s	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land n \in ℤ) \to n \underset{˙}{\cdot} \underset{˙}{1} \in B$
10	9 2	fmptd	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to F : ℤ ⟶ B$
11		eqid	$⊢ +_{R} = +_{R}$
12	3 1 11	mulgdir	$⊢ (R \in Grp \land (x \in ℤ \land y \in ℤ \land \underset{˙}{1} \in B)) \to (x + y) \underset{˙}{\cdot} \underset{˙}{1} = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
13	12	3exp2	$⊢ R \in Grp \to (x \in ℤ \to (y \in ℤ \to (\underset{˙}{1} \in B \to (x + y) \underset{˙}{\cdot} \underset{˙}{1} = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1}))))$
14	13	imp42	$⊢ ((R \in Grp \land (x \in ℤ \land y \in ℤ)) \land \underset{˙}{1} \in B) \to (x + y) \underset{˙}{\cdot} \underset{˙}{1} = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
15	14	an32s	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land (x \in ℤ \land y \in ℤ)) \to (x + y) \underset{˙}{\cdot} \underset{˙}{1} = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
16		zaddcl	$⊢ (x \in ℤ \land y \in ℤ) \to x + y \in ℤ$
17	16	adantl	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land (x \in ℤ \land y \in ℤ)) \to x + y \in ℤ$
18		oveq1	$⊢ n = x + y \to n \underset{˙}{\cdot} \underset{˙}{1} = (x + y) \underset{˙}{\cdot} \underset{˙}{1}$
19		ovex	$⊢ (x + y) \underset{˙}{\cdot} \underset{˙}{1} \in V$
20	18 2 19	fvmpt	$⊢ x + y \in ℤ \to F (x + y) = (x + y) \underset{˙}{\cdot} \underset{˙}{1}$
21	17 20	syl	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land (x \in ℤ \land y \in ℤ)) \to F (x + y) = (x + y) \underset{˙}{\cdot} \underset{˙}{1}$
22		oveq1	$⊢ n = x \to n \underset{˙}{\cdot} \underset{˙}{1} = x \underset{˙}{\cdot} \underset{˙}{1}$
23		ovex	$⊢ x \underset{˙}{\cdot} \underset{˙}{1} \in V$
24	22 2 23	fvmpt	$⊢ x \in ℤ \to F (x) = x \underset{˙}{\cdot} \underset{˙}{1}$
25		oveq1	$⊢ n = y \to n \underset{˙}{\cdot} \underset{˙}{1} = y \underset{˙}{\cdot} \underset{˙}{1}$
26		ovex	$⊢ y \underset{˙}{\cdot} \underset{˙}{1} \in V$
27	25 2 26	fvmpt	$⊢ y \in ℤ \to F (y) = y \underset{˙}{\cdot} \underset{˙}{1}$
28	24 27	oveqan12d	$⊢ (x \in ℤ \land y \in ℤ) \to F (x) +_{R} F (y) = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
29	28	adantl	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land (x \in ℤ \land y \in ℤ)) \to F (x) +_{R} F (y) = (x \underset{˙}{\cdot} \underset{˙}{1}) +_{R} (y \underset{˙}{\cdot} \underset{˙}{1})$
30	15 21 29	3eqtr4d	$⊢ ((R \in Grp \land \underset{˙}{1} \in B) \land (x \in ℤ \land y \in ℤ)) \to F (x + y) = F (x) +_{R} F (y)$
31	30	ralrimivva	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to \forall x \in ℤ \forall y \in ℤ F (x + y) = F (x) +_{R} F (y)$
32	10 31	jca	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to (F : ℤ ⟶ B \land \forall x \in ℤ \forall y \in ℤ F (x + y) = F (x) +_{R} F (y))$
33		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
34		zringplusg	$⊢ + = +_{ℤ_{ring}}$
35	33 3 34 11	isghm	$⊢ F \in (ℤ_{ring} GrpHom R) \leftrightarrow ((ℤ_{ring} \in Grp \land R \in Grp) \land (F : ℤ ⟶ B \land \forall x \in ℤ \forall y \in ℤ F (x + y) = F (x) +_{R} F (y)))$
36	6 32 35	sylanbrc	$⊢ (R \in Grp \land \underset{˙}{1} \in B) \to F \in (ℤ_{ring} GrpHom R)$

Metamath Proof Explorer

Theorem mulgghm2

Proof