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 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑁 · 𝑋 ) ) = ( 𝑁 × ( 𝐹 ‘ 𝑋 ) ) )