Metamath Proof Explorer

Theorem ghmmulg

Description: A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015)

Ref Expression
Hypotheses ghmmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ghmmulg.s ⊢ · = ( .g ‘ 𝐺 )
ghmmulg.t ⊢ × = ( .g ‘ 𝐻 )
Assertion ghmmulg ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 ghmmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ghmmulg.s ⊢ · = ( .g ‘ 𝐺 )
3 ghmmulg.t ⊢ × = ( .g ‘ 𝐻 )
4 ghmmhm ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )
5 1 2 3 mhmmulg ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
6 4 5 syl3an1 ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
7 6 3expa ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
8 7 an32s ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
9 8 3adantl2 ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
10 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
11 10 4 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )
12 nnnn0 ⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
13 12 ad2antll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℕ0 )
14 simpl3 ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑋 ∈ 𝐵 )
15 1 2 3 mhmmulg ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ - 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( - 𝑁 · 𝑋 ) ) = ( - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
16 11 13 14 15 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( - 𝑁 · 𝑋 ) ) = ( - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
17 16 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ ( - 𝑁 · 𝑋 ) ) ) = ( ( invg ‘ 𝐻 ) ‘ ( - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) )
18 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
19 10 18 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐺 ∈ Grp )
20 nnz ⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
21 20 ad2antll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - 𝑁 ∈ ℤ )
22 1 2 mulgcl ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
23 19 21 14 22 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - 𝑁 · 𝑋 ) ∈ 𝐵 )
24 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
25 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
26 1 24 25 ghminv ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( - 𝑁 · 𝑋 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) = ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ ( - 𝑁 · 𝑋 ) ) ) )
27 10 23 26 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) = ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ ( - 𝑁 · 𝑋 ) ) ) )
28 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐻 ∈ Grp )
29 10 28 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐻 ∈ Grp )
30 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
31 1 30 ghmf ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
32 10 31 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
33 32 14 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) )
34 30 3 25 mulgneg ⊢ ( ( 𝐻 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) ) → ( - - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) )
35 29 21 33 34 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) )
36 17 27 35 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) = ( - - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
37 1 2 24 mulgneg ⊢ ( ( 𝐺 ∈ Grp ∧ - 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( - - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) )
38 19 21 14 37 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 · 𝑋 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) )
39 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℝ )
40 39 recnd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → 𝑁 ∈ ℂ )
41 40 negnegd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → - - 𝑁 = 𝑁 )
42 41 oveq1d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 · 𝑋 ) = ( 𝑁 · 𝑋 ) )
43 38 42 eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) = ( 𝑁 · 𝑋 ) )
44 43 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑋 ) ) ) = ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) )
45 36 44 eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) )
46 41 oveq1d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( - - 𝑁 × ( 𝐹 ‘ 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
47 45 46 eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
48 simp2 ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
49 elznn0nn ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
50 48 49 sylib ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
51 9 47 50 mpjaodan ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )