Metamath Proof Explorer

Theorem mhmmulg

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

Ref Expression
Hypotheses mhmmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mhmmulg.s ⊢ · = ( .g ‘ 𝐺 )
mhmmulg.t ⊢ × = ( .g ‘ 𝐻 )
Assertion mhmmulg ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 mhmmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mhmmulg.s ⊢ · = ( .g ‘ 𝐺 )
3 mhmmulg.t ⊢ × = ( .g ‘ 𝐻 )
4 fvoveq1 ⊢ ( 𝑛 = 0 → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝐹 ‘ ( 0 · 𝑋 ) ) )
5 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) = ( 0 × ( 𝐹 ‘ 𝑋 ) ) )
6 4 5 eqeq12d ⊢ ( 𝑛 = 0 → ( ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ↔ ( 𝐹 ‘ ( 0 · 𝑋 ) ) = ( 0 × ( 𝐹 ‘ 𝑋 ) ) ) )
7 6 imbi2d ⊢ ( 𝑛 = 0 → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0 · 𝑋 ) ) = ( 0 × ( 𝐹 ‘ 𝑋 ) ) ) ) )
8 fvoveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) )
9 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) )
10 8 9 eqeq12d ⊢ ( 𝑛 = 𝑚 → ( ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ↔ ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ) )
11 10 imbi2d ⊢ ( 𝑛 = 𝑚 → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ) ) )
12 fvoveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) )
13 oveq1 ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) )
14 12 13 eqeq12d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ↔ ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ) )
15 14 imbi2d ⊢ ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ) ) )
16 fvoveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) )
17 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
18 16 17 eqeq12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ↔ ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) )
19 18 imbi2d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑛 · 𝑋 ) ) = ( 𝑛 × ( 𝐹 ‘ 𝑋 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) ) )
20 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
21 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
22 20 21 mhm0 ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) = ( 0g ‘ 𝐻 ) )
24 1 20 2 mulg0 ⊢ ( 𝑋 ∈ 𝐵 → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
25 24 adantl ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝐺 ) )
26 25 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0 · 𝑋 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝐺 ) ) )
27 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
28 1 27 mhmf ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
29 28 ffvelrnda ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) )
30 27 21 3 mulg0 ⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) → ( 0 × ( 𝐹 ‘ 𝑋 ) ) = ( 0g ‘ 𝐻 ) )
31 29 30 syl ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 0 × ( 𝐹 ‘ 𝑋 ) ) = ( 0g ‘ 𝐻 ) )
32 23 26 31 3eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 0 · 𝑋 ) ) = ( 0 × ( 𝐹 ‘ 𝑋 ) ) )
33 oveq1 ⊢ ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) → ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
34 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐺 ∈ Mnd )
35 34 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐺 ∈ Mnd )
36 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝑚 ∈ ℕ0 )
37 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
38 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
39 1 2 38 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑚 + 1 ) · 𝑋 ) = ( ( 𝑚 · 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) )
40 35 36 37 39 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) · 𝑋 ) = ( ( 𝑚 · 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) )
41 40 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( 𝐹 ‘ ( ( 𝑚 · 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ) )
42 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) )
43 34 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
44 simplr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑚 ∈ ℕ0 )
45 simpr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
46 1 2 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
48 47 an32s ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
49 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
50 1 38 49 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ ( 𝑚 · 𝑋 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑚 · 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
51 42 48 37 50 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑚 · 𝑋 ) ( +g ‘ 𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
52 41 51 eqtrd ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
53 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐻 ∈ Mnd )
54 53 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐻 ∈ Mnd )
55 29 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) )
56 27 3 49 mulgnn0p1 ⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑚 ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
57 54 36 55 56 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
58 52 57 eqeq12d ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ↔ ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) ) )
59 33 58 syl5ibr ⊢ ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ) )
60 59 expcom ⊢ ( 𝑚 ∈ ℕ0 → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ) ) )
61 60 a2d ⊢ ( 𝑚 ∈ ℕ0 → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹 ‘ 𝑋 ) ) ) → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹 ‘ 𝑋 ) ) ) ) )
62 7 11 15 19 32 61 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) ) )
63 62 3impib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )
64 63 3com12 ⊢ ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )