Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑅 ∈ 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 𝑅 ) )