Metamath Proof Explorer


Theorem mhmmnd

Description: The image of a monoid G under a monoid homomorphism F is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f φ x X y X F x + ˙ y = F x ˙ F y
ghmgrp.x X = Base G
ghmgrp.y Y = Base H
ghmgrp.p + ˙ = + G
ghmgrp.q ˙ = + H
ghmgrp.1 φ F : X onto Y
mhmmnd.3 φ G Mnd
Assertion mhmmnd φ H Mnd

Proof

Step Hyp Ref Expression
1 ghmgrp.f φ x X y X F x + ˙ y = F x ˙ F y
2 ghmgrp.x X = Base G
3 ghmgrp.y Y = Base H
4 ghmgrp.p + ˙ = + G
5 ghmgrp.q ˙ = + H
6 ghmgrp.1 φ F : X onto Y
7 mhmmnd.3 φ G Mnd
8 simpllr φ a Y b Y i X F i = a j X F j = b F i = a
9 simpr φ a Y b Y i X F i = a j X F j = b F j = b
10 8 9 oveq12d φ a Y b Y i X F i = a j X F j = b F i ˙ F j = a ˙ b
11 simp-5l φ a Y b Y i X F i = a j X F j = b φ
12 11 1 syl3an1 φ a Y b Y i X F i = a j X F j = b x X y X F x + ˙ y = F x ˙ F y
13 simp-4r φ a Y b Y i X F i = a j X F j = b i X
14 simplr φ a Y b Y i X F i = a j X F j = b j X
15 12 13 14 mhmlem φ a Y b Y i X F i = a j X F j = b F i + ˙ j = F i ˙ F j
16 fof F : X onto Y F : X Y
17 6 16 syl φ F : X Y
18 17 ad5antr φ a Y b Y i X F i = a j X F j = b F : X Y
19 7 ad5antr φ a Y b Y i X F i = a j X F j = b G Mnd
20 2 4 mndcl G Mnd i X j X i + ˙ j X
21 19 13 14 20 syl3anc φ a Y b Y i X F i = a j X F j = b i + ˙ j X
22 18 21 ffvelrnd φ a Y b Y i X F i = a j X F j = b F i + ˙ j Y
23 15 22 eqeltrrd φ a Y b Y i X F i = a j X F j = b F i ˙ F j Y
24 10 23 eqeltrrd φ a Y b Y i X F i = a j X F j = b a ˙ b Y
25 simpr a Y b Y b Y
26 foelrni F : X onto Y b Y j X F j = b
27 6 25 26 syl2an φ a Y b Y j X F j = b
28 27 ad2antrr φ a Y b Y i X F i = a j X F j = b
29 24 28 r19.29a φ a Y b Y i X F i = a a ˙ b Y
30 simpl a Y b Y a Y
31 foelrni F : X onto Y a Y i X F i = a
32 6 30 31 syl2an φ a Y b Y i X F i = a
33 29 32 r19.29a φ a Y b Y a ˙ b Y
34 simpll φ a Y b Y c Y φ
35 simplrl φ a Y b Y c Y a Y
36 simplrr φ a Y b Y c Y b Y
37 simpr φ a Y b Y c Y c Y
38 7 ad2antrr φ a Y b Y c Y i X G Mnd
39 38 ad5antr φ a Y b Y c Y i X F i = a j X F j = b k X F k = c G Mnd
40 simp-6r φ a Y b Y c Y i X F i = a j X F j = b k X F k = c i X
41 simp-4r φ a Y b Y c Y i X F i = a j X F j = b k X F k = c j X
42 simplr φ a Y b Y c Y i X F i = a j X F j = b k X F k = c k X
43 2 4 mndass G Mnd i X j X k X i + ˙ j + ˙ k = i + ˙ j + ˙ k
44 39 40 41 42 43 syl13anc φ a Y b Y c Y i X F i = a j X F j = b k X F k = c i + ˙ j + ˙ k = i + ˙ j + ˙ k
45 44 fveq2d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j + ˙ k = F i + ˙ j + ˙ k
46 simp-7l φ a Y b Y c Y i X F i = a j X F j = b k X F k = c φ
47 46 1 syl3an1 φ a Y b Y c Y i X F i = a j X F j = b k X F k = c x X y X F x + ˙ y = F x ˙ F y
48 39 40 41 20 syl3anc φ a Y b Y c Y i X F i = a j X F j = b k X F k = c i + ˙ j X
49 47 48 42 mhmlem φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j + ˙ k = F i + ˙ j ˙ F k
50 2 4 mndcl G Mnd j X k X j + ˙ k X
51 39 41 42 50 syl3anc φ a Y b Y c Y i X F i = a j X F j = b k X F k = c j + ˙ k X
52 47 40 51 mhmlem φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j + ˙ k = F i ˙ F j + ˙ k
53 45 49 52 3eqtr3d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j ˙ F k = F i ˙ F j + ˙ k
54 simp1 φ i X j X φ
55 54 1 syl3an1 φ i X j X x X y X F x + ˙ y = F x ˙ F y
56 simp2 φ i X j X i X
57 simp3 φ i X j X j X
58 55 56 57 mhmlem φ i X j X F i + ˙ j = F i ˙ F j
59 46 40 41 58 syl3anc φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j = F i ˙ F j
60 59 oveq1d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i + ˙ j ˙ F k = F i ˙ F j ˙ F k
61 47 41 42 mhmlem φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F j + ˙ k = F j ˙ F k
62 61 oveq2d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i ˙ F j + ˙ k = F i ˙ F j ˙ F k
63 53 60 62 3eqtr3d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i ˙ F j ˙ F k = F i ˙ F j ˙ F k
64 simp-5r φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i = a
65 simpllr φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F j = b
66 64 65 oveq12d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i ˙ F j = a ˙ b
67 simpr φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F k = c
68 66 67 oveq12d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i ˙ F j ˙ F k = a ˙ b ˙ c
69 65 67 oveq12d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F j ˙ F k = b ˙ c
70 64 69 oveq12d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c F i ˙ F j ˙ F k = a ˙ b ˙ c
71 63 68 70 3eqtr3d φ a Y b Y c Y i X F i = a j X F j = b k X F k = c a ˙ b ˙ c = a ˙ b ˙ c
72 foelrni F : X onto Y c Y k X F k = c
73 6 72 sylan φ c Y k X F k = c
74 73 3ad2antr3 φ a Y b Y c Y k X F k = c
75 74 ad4antr φ a Y b Y c Y i X F i = a j X F j = b k X F k = c
76 71 75 r19.29a φ a Y b Y c Y i X F i = a j X F j = b a ˙ b ˙ c = a ˙ b ˙ c
77 27 3adantr3 φ a Y b Y c Y j X F j = b
78 77 ad2antrr φ a Y b Y c Y i X F i = a j X F j = b
79 76 78 r19.29a φ a Y b Y c Y i X F i = a a ˙ b ˙ c = a ˙ b ˙ c
80 32 3adantr3 φ a Y b Y c Y i X F i = a
81 79 80 r19.29a φ a Y b Y c Y a ˙ b ˙ c = a ˙ b ˙ c
82 34 35 36 37 81 syl13anc φ a Y b Y c Y a ˙ b ˙ c = a ˙ b ˙ c
83 82 ralrimiva φ a Y b Y c Y a ˙ b ˙ c = a ˙ b ˙ c
84 33 83 jca φ a Y b Y a ˙ b Y c Y a ˙ b ˙ c = a ˙ b ˙ c
85 84 ralrimivva φ a Y b Y a ˙ b Y c Y a ˙ b ˙ c = a ˙ b ˙ c
86 eqid 0 G = 0 G
87 2 86 mndidcl G Mnd 0 G X
88 7 87 syl φ 0 G X
89 17 88 ffvelrnd φ F 0 G Y
90 simplll φ a Y i X F i = a φ
91 90 1 syl3an1 φ a Y i X F i = a x X y X F x + ˙ y = F x ˙ F y
92 7 ad3antrrr φ a Y i X F i = a G Mnd
93 92 87 syl φ a Y i X F i = a 0 G X
94 simplr φ a Y i X F i = a i X
95 91 93 94 mhmlem φ a Y i X F i = a F 0 G + ˙ i = F 0 G ˙ F i
96 2 4 86 mndlid G Mnd i X 0 G + ˙ i = i
97 92 94 96 syl2anc φ a Y i X F i = a 0 G + ˙ i = i
98 97 fveq2d φ a Y i X F i = a F 0 G + ˙ i = F i
99 95 98 eqtr3d φ a Y i X F i = a F 0 G ˙ F i = F i
100 simpr φ a Y i X F i = a F i = a
101 100 oveq2d φ a Y i X F i = a F 0 G ˙ F i = F 0 G ˙ a
102 99 101 100 3eqtr3d φ a Y i X F i = a F 0 G ˙ a = a
103 91 94 93 mhmlem φ a Y i X F i = a F i + ˙ 0 G = F i ˙ F 0 G
104 2 4 86 mndrid G Mnd i X i + ˙ 0 G = i
105 92 94 104 syl2anc φ a Y i X F i = a i + ˙ 0 G = i
106 105 fveq2d φ a Y i X F i = a F i + ˙ 0 G = F i
107 103 106 eqtr3d φ a Y i X F i = a F i ˙ F 0 G = F i
108 100 oveq1d φ a Y i X F i = a F i ˙ F 0 G = a ˙ F 0 G
109 107 108 100 3eqtr3d φ a Y i X F i = a a ˙ F 0 G = a
110 102 109 jca φ a Y i X F i = a F 0 G ˙ a = a a ˙ F 0 G = a
111 6 31 sylan φ a Y i X F i = a
112 110 111 r19.29a φ a Y F 0 G ˙ a = a a ˙ F 0 G = a
113 112 ralrimiva φ a Y F 0 G ˙ a = a a ˙ F 0 G = a
114 oveq1 d = F 0 G d ˙ a = F 0 G ˙ a
115 114 eqeq1d d = F 0 G d ˙ a = a F 0 G ˙ a = a
116 115 ovanraleqv d = F 0 G a Y d ˙ a = a a ˙ d = a a Y F 0 G ˙ a = a a ˙ F 0 G = a
117 116 rspcev F 0 G Y a Y F 0 G ˙ a = a a ˙ F 0 G = a d Y a Y d ˙ a = a a ˙ d = a
118 89 113 117 syl2anc φ d Y a Y d ˙ a = a a ˙ d = a
119 3 5 ismnd H Mnd a Y b Y a ˙ b Y c Y a ˙ b ˙ c = a ˙ b ˙ c d Y a Y d ˙ a = a a ˙ d = a
120 85 118 119 sylanbrc φ H Mnd