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 ffvelcdmda ( ( 𝐹 ∈ ( 𝐺 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 43 44 45 mulgnn0cld ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑚 ∈ ℕ0 ) ∧ 𝑋𝐵 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
47 46 an32s ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 · 𝑋 ) ∈ 𝐵 )
48 eqid ( +g𝐻 ) = ( +g𝐻 )
49 1 38 48 mhmlin ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ ( 𝑚 · 𝑋 ) ∈ 𝐵𝑋𝐵 ) → ( 𝐹 ‘ ( ( 𝑚 · 𝑋 ) ( +g𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) )
50 42 47 37 49 syl3anc ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑚 · 𝑋 ) ( +g𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) )
51 41 50 eqtrd ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) )
52 mhmrcl2 ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) → 𝐻 ∈ Mnd )
53 52 ad2antrr ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → 𝐻 ∈ Mnd )
54 29 adantr ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝐹𝑋 ) ∈ ( Base ‘ 𝐻 ) )
55 27 3 48 mulgnn0p1 ( ( 𝐻 ∈ Mnd ∧ 𝑚 ∈ ℕ0 ∧ ( 𝐹𝑋 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) = ( ( 𝑚 × ( 𝐹𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) )
56 53 36 54 55 syl3anc ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) = ( ( 𝑚 × ( 𝐹𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) )
57 51 56 eqeq12d ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) ↔ ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) = ( ( 𝑚 × ( 𝐹𝑋 ) ) ( +g𝐻 ) ( 𝐹𝑋 ) ) ) )
58 33 57 imbitrrid ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) ) )
59 58 expcom ( 𝑚 ∈ ℕ0 → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) → ( ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) ) ) )
60 59 a2d ( 𝑚 ∈ ℕ0 → ( ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐹 ‘ ( 𝑚 · 𝑋 ) ) = ( 𝑚 × ( 𝐹𝑋 ) ) ) → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐹 ‘ ( ( 𝑚 + 1 ) · 𝑋 ) ) = ( ( 𝑚 + 1 ) × ( 𝐹𝑋 ) ) ) ) )
61 7 11 15 19 32 60 nn0ind ( 𝑁 ∈ ℕ0 → ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹𝑋 ) ) ) )
62 61 3impib ( ( 𝑁 ∈ ℕ0𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑋𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹𝑋 ) ) )
63 62 3com12 ( ( 𝐹 ∈ ( 𝐺 MndHom 𝐻 ) ∧ 𝑁 ∈ ℕ0𝑋𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹𝑋 ) ) )