Metamath Proof Explorer

Theorem 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 ⊢ · = ( .g ‘ 𝑅 )
mulgghm2.f ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
mulgghm2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion mulgghm2 ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → 𝐹 ∈ ( ℤring GrpHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mulgghm2.m ⊢ · = ( .g ‘ 𝑅 )
2 mulgghm2.f ⊢ 𝐹 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
3 mulgghm2.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 simpl ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → 𝑅 ∈ Grp )
5 zringgrp ⊢ ℤring ∈ Grp
6 4 5 jctil ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( ℤring ∈ Grp ∧ 𝑅 ∈ Grp ) )
7 3 1 mulgcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 1 ∈ 𝐵 ) → ( 𝑛 · 1 ) ∈ 𝐵 )
8 7 3expa ⊢ ( ( ( 𝑅 ∈ Grp ∧ 𝑛 ∈ ℤ ) ∧ 1 ∈ 𝐵 ) → ( 𝑛 · 1 ) ∈ 𝐵 )
9 8 an32s ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 1 ) ∈ 𝐵 )
10 9 2 fmptd ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → 𝐹 : ℤ ⟶ 𝐵 )
11 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
12 3 1 11 mulgdir ⊢ ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 1 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) · 1 ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
13 12 3exp2 ⊢ ( 𝑅 ∈ Grp → ( 𝑥 ∈ ℤ → ( 𝑦 ∈ ℤ → ( 1 ∈ 𝐵 → ( ( 𝑥 + 𝑦 ) · 1 ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) ) ) ) )
14 13 imp42 ⊢ ( ( ( 𝑅 ∈ Grp ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) ∧ 1 ∈ 𝐵 ) → ( ( 𝑥 + 𝑦 ) · 1 ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
15 14 an32s ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 + 𝑦 ) · 1 ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
16 zaddcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
17 16 adantl ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 + 𝑦 ) ∈ ℤ )
18 oveq1 ⊢ ( 𝑛 = ( 𝑥 + 𝑦 ) → ( 𝑛 · 1 ) = ( ( 𝑥 + 𝑦 ) · 1 ) )
19 ovex ⊢ ( ( 𝑥 + 𝑦 ) · 1 ) ∈ V
20 18 2 19 fvmpt ⊢ ( ( 𝑥 + 𝑦 ) ∈ ℤ → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑥 + 𝑦 ) · 1 ) )
21 17 20 syl ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝑥 + 𝑦 ) · 1 ) )
22 oveq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 · 1 ) = ( 𝑥 · 1 ) )
23 ovex ⊢ ( 𝑥 · 1 ) ∈ V
24 22 2 23 fvmpt ⊢ ( 𝑥 ∈ ℤ → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 · 1 ) )
25 oveq1 ⊢ ( 𝑛 = 𝑦 → ( 𝑛 · 1 ) = ( 𝑦 · 1 ) )
26 ovex ⊢ ( 𝑦 · 1 ) ∈ V
27 25 2 26 fvmpt ⊢ ( 𝑦 ∈ ℤ → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 1 ) )
28 24 27 oveqan12d ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
29 28 adantl ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝑥 · 1 ) ( +g ‘ 𝑅 ) ( 𝑦 · 1 ) ) )
30 15 21 29 3eqtr4d ⊢ ( ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
31 30 ralrimivva ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) )
32 10 31 jca ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → ( 𝐹 : ℤ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) ) )
33 zringbas ⊢ ℤ = ( Base ‘ ℤring )
34 zringplusg ⊢ + = ( +g ‘ ℤring )
35 33 3 34 11 isghm ⊢ ( 𝐹 ∈ ( ℤring GrpHom 𝑅 ) ↔ ( ( ℤring ∈ Grp ∧ 𝑅 ∈ Grp ) ∧ ( 𝐹 : ℤ ⟶ 𝐵 ∧ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
36 6 32 35 sylanbrc ⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ 𝐵 ) → 𝐹 ∈ ( ℤring GrpHom 𝑅 ) )