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 B = Base G
mhmmulg.s · ˙ = G
mhmmulg.t × ˙ = H
Assertion mhmmulg F G MndHom H N 0 X B F N · ˙ X = N × ˙ F X

Proof

Step Hyp Ref Expression
1 mhmmulg.b B = Base G
2 mhmmulg.s · ˙ = G
3 mhmmulg.t × ˙ = H
4 fvoveq1 n = 0 F n · ˙ X = F 0 · ˙ X
5 oveq1 n = 0 n × ˙ F X = 0 × ˙ F X
6 4 5 eqeq12d n = 0 F n · ˙ X = n × ˙ F X F 0 · ˙ X = 0 × ˙ F X
7 6 imbi2d n = 0 F G MndHom H X B F n · ˙ X = n × ˙ F X F G MndHom H X B F 0 · ˙ X = 0 × ˙ F X
8 fvoveq1 n = m F n · ˙ X = F m · ˙ X
9 oveq1 n = m n × ˙ F X = m × ˙ F X
10 8 9 eqeq12d n = m F n · ˙ X = n × ˙ F X F m · ˙ X = m × ˙ F X
11 10 imbi2d n = m F G MndHom H X B F n · ˙ X = n × ˙ F X F G MndHom H X B F m · ˙ X = m × ˙ F X
12 fvoveq1 n = m + 1 F n · ˙ X = F m + 1 · ˙ X
13 oveq1 n = m + 1 n × ˙ F X = m + 1 × ˙ F X
14 12 13 eqeq12d n = m + 1 F n · ˙ X = n × ˙ F X F m + 1 · ˙ X = m + 1 × ˙ F X
15 14 imbi2d n = m + 1 F G MndHom H X B F n · ˙ X = n × ˙ F X F G MndHom H X B F m + 1 · ˙ X = m + 1 × ˙ F X
16 fvoveq1 n = N F n · ˙ X = F N · ˙ X
17 oveq1 n = N n × ˙ F X = N × ˙ F X
18 16 17 eqeq12d n = N F n · ˙ X = n × ˙ F X F N · ˙ X = N × ˙ F X
19 18 imbi2d n = N F G MndHom H X B F n · ˙ X = n × ˙ F X F G MndHom H X B F N · ˙ X = N × ˙ F X
20 eqid 0 G = 0 G
21 eqid 0 H = 0 H
22 20 21 mhm0 F G MndHom H F 0 G = 0 H
23 22 adantr F G MndHom H X B F 0 G = 0 H
24 1 20 2 mulg0 X B 0 · ˙ X = 0 G
25 24 adantl F G MndHom H X B 0 · ˙ X = 0 G
26 25 fveq2d F G MndHom H X B F 0 · ˙ X = F 0 G
27 eqid Base H = Base H
28 1 27 mhmf F G MndHom H F : B Base H
29 28 ffvelcdmda F G MndHom H X B F X Base H
30 27 21 3 mulg0 F X Base H 0 × ˙ F X = 0 H
31 29 30 syl F G MndHom H X B 0 × ˙ F X = 0 H
32 23 26 31 3eqtr4d F G MndHom H X B F 0 · ˙ X = 0 × ˙ F X
33 oveq1 F m · ˙ X = m × ˙ F X F m · ˙ X + H F X = m × ˙ F X + H F X
34 mhmrcl1 F G MndHom H G Mnd
35 34 ad2antrr F G MndHom H X B m 0 G Mnd
36 simpr F G MndHom H X B m 0 m 0
37 simplr F G MndHom H X B m 0 X B
38 eqid + G = + G
39 1 2 38 mulgnn0p1 G Mnd m 0 X B m + 1 · ˙ X = m · ˙ X + G X
40 35 36 37 39 syl3anc F G MndHom H X B m 0 m + 1 · ˙ X = m · ˙ X + G X
41 40 fveq2d F G MndHom H X B m 0 F m + 1 · ˙ X = F m · ˙ X + G X
42 simpll F G MndHom H X B m 0 F G MndHom H
43 34 ad2antrr F G MndHom H m 0 X B G Mnd
44 simplr F G MndHom H m 0 X B m 0
45 simpr F G MndHom H m 0 X B X B
46 1 2 43 44 45 mulgnn0cld F G MndHom H m 0 X B m · ˙ X B
47 46 an32s F G MndHom H X B m 0 m · ˙ X B
48 eqid + H = + H
49 1 38 48 mhmlin F G MndHom H m · ˙ X B X B F m · ˙ X + G X = F m · ˙ X + H F X
50 42 47 37 49 syl3anc F G MndHom H X B m 0 F m · ˙ X + G X = F m · ˙ X + H F X
51 41 50 eqtrd F G MndHom H X B m 0 F m + 1 · ˙ X = F m · ˙ X + H F X
52 mhmrcl2 F G MndHom H H Mnd
53 52 ad2antrr F G MndHom H X B m 0 H Mnd
54 29 adantr F G MndHom H X B m 0 F X Base H
55 27 3 48 mulgnn0p1 H Mnd m 0 F X Base H m + 1 × ˙ F X = m × ˙ F X + H F X
56 53 36 54 55 syl3anc F G MndHom H X B m 0 m + 1 × ˙ F X = m × ˙ F X + H F X
57 51 56 eqeq12d F G MndHom H X B m 0 F m + 1 · ˙ X = m + 1 × ˙ F X F m · ˙ X + H F X = m × ˙ F X + H F X
58 33 57 imbitrrid F G MndHom H X B m 0 F m · ˙ X = m × ˙ F X F m + 1 · ˙ X = m + 1 × ˙ F X
59 58 expcom m 0 F G MndHom H X B F m · ˙ X = m × ˙ F X F m + 1 · ˙ X = m + 1 × ˙ F X
60 59 a2d m 0 F G MndHom H X B F m · ˙ X = m × ˙ F X F G MndHom H X B F m + 1 · ˙ X = m + 1 × ˙ F X
61 7 11 15 19 32 60 nn0ind N 0 F G MndHom H X B F N · ˙ X = N × ˙ F X
62 61 3impib N 0 F G MndHom H X B F N · ˙ X = N × ˙ F X
63 62 3com12 F G MndHom H N 0 X B F N · ˙ X = N × ˙ F X