Theorem mulgrhm

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

	Ref	Expression
Hypotheses	mulgghm2.m	⊢ · = ( .g ‘ 𝑅 )
	mulgghm2.f	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
	mulgrhm.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	mulgrhm	⊢ ( 𝑅 ∈ Ring → 𝐹 ∈ ( ℤring RingHom 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgghm2.m	⊢ · = ( .g ‘ 𝑅 )
2		mulgghm2.f	⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
3		mulgrhm.1	⊢ 1 = ( 1r ‘ 𝑅 )
4		zringbas	⊢ ℤ = ( Base ‘ ℤring )
5		zring1	⊢ 1 = ( 1r ‘ ℤring )
6		zringmulr	⊢ · = ( .r ‘ ℤring )
7		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8		zringring	⊢ ℤring ∈ Ring
9	8	a1i	⊢ ( 𝑅 ∈ Ring → ℤring ∈ Ring )
10		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
11		1z	⊢ 1 ∈ ℤ
12		oveq1	⊢ ( 𝑛 = 1 → ( 𝑛 · 1 ) = ( 1 · 1 ) )
13		ovex	⊢ ( 1 · 1 ) ∈ V
14	12 2 13	fvmpt	⊢ ( 1 ∈ ℤ → ( 𝐹 ‘ 1 ) = ( 1 · 1 ) )
15	11 14	ax-mp	⊢ ( 𝐹 ‘ 1 ) = ( 1 · 1 )
16		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17	16 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
18	16 1	mulg1	⊢ ( 1 ∈ ( Base ‘ 𝑅 ) → ( 1 · 1 ) = 1 )
19	17 18	syl	⊢ ( 𝑅 ∈ Ring → ( 1 · 1 ) = 1 )
20	15 19	eqtrid	⊢ ( 𝑅 ∈ Ring → ( 𝐹 ‘ 1 ) = 1 )
21		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
22	21	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑅 ∈ Grp )
23		simprr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
24	17	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 1 ∈ ( Base ‘ 𝑅 ) )
25	16 1	mulgcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 · 1 ) ∈ ( Base ‘ 𝑅 ) )
26	22 23 24 25	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑦 · 1 ) ∈ ( Base ‘ 𝑅 ) )
27	16 7 3	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 · 1 ) ∈ ( Base ‘ 𝑅 ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) = ( 𝑦 · 1 ) )
28	26 27	syldan	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 1 ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) = ( 𝑦 · 1 ) )
29	28	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · ( 1 ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) ) = ( 𝑥 · ( 𝑦 · 1 ) ) )
30		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑅 ∈ Ring )
31		simprl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
32	16 1 7	mulgass2	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 1 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑦 · 1 ) ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 · 1 ) ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) = ( 𝑥 · ( 1 ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) ) )
33	30 31 24 26 32	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 1 ) ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) = ( 𝑥 · ( 1 ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) ) )
34	16 1	mulgass	⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 · 𝑦 ) · 1 ) = ( 𝑥 · ( 𝑦 · 1 ) ) )
35	22 31 23 24 34	syl13anc	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑦 ) · 1 ) = ( 𝑥 · ( 𝑦 · 1 ) ) )
36	29 33 35	3eqtr4rd	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑦 ) · 1 ) = ( ( 𝑥 · 1 ) ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
37		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
38	37	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑦 ) ∈ ℤ )
39		oveq1	⊢ ( 𝑛 = ( 𝑥 · 𝑦 ) → ( 𝑛 · 1 ) = ( ( 𝑥 · 𝑦 ) · 1 ) )
40		ovex	⊢ ( ( 𝑥 · 𝑦 ) · 1 ) ∈ V
41	39 2 40	fvmpt	⊢ ( ( 𝑥 · 𝑦 ) ∈ ℤ → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) · 1 ) )
42	38 41	syl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝑥 · 𝑦 ) · 1 ) )
43		oveq1	⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 1 ) = ( 𝑥 · 1 ) )
44		ovex	⊢ ( 𝑥 · 1 ) ∈ V
45	43 2 44	fvmpt	⊢ ( 𝑥 ∈ ℤ → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 · 1 ) )
46		oveq1	⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 1 ) = ( 𝑦 · 1 ) )
47		ovex	⊢ ( 𝑦 · 1 ) ∈ V
48	46 2 47	fvmpt	⊢ ( 𝑦 ∈ ℤ → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 1 ) )
49	45 48	oveqan12d	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 · 1 ) ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
50	49	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 · 1 ) ( .r ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
51	36 42 50	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑥 · 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
52	1 2 16	mulgghm2	⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → 𝐹 ∈ ( ℤring GrpHom 𝑅 ) )
53	21 17 52	syl2anc	⊢ ( 𝑅 ∈ Ring → 𝐹 ∈ ( ℤring GrpHom 𝑅 ) )
54	4 5 3 6 7 9 10 20 51 53	isrhm2d	⊢ ( 𝑅 ∈ Ring → 𝐹 ∈ ( ℤring RingHom 𝑅 ) )