Theorem mulgghm2

Description: The powers of a group element give a homomorphism from ZZ to a group. The name .1. should not be taken as a constraint as it may be any group element. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypotheses	mulgghm2.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	mulgghm2.f	$$⊢F=\left(n\in \mathbb{Z}⟼n\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
	mulgghm2.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	mulgghm2	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in B\right)\to F\in \left({\mathbb{Z}}_{\mathrm{ring}}\mathrm{GrpHom}R\right)$$

Proof

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