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 φxXyXFx+˙y=Fx˙Fy
ghmgrp.x X=BaseG
ghmgrp.y Y=BaseH
ghmgrp.p +˙=+G
ghmgrp.q ˙=+H
ghmgrp.1 φF:XontoY
mhmmnd.3 φGMnd
Assertion mhmmnd φHMnd

Proof

Step Hyp Ref Expression
1 ghmgrp.f φxXyXFx+˙y=Fx˙Fy
2 ghmgrp.x X=BaseG
3 ghmgrp.y Y=BaseH
4 ghmgrp.p +˙=+G
5 ghmgrp.q ˙=+H
6 ghmgrp.1 φF:XontoY
7 mhmmnd.3 φGMnd
8 simpllr φaYbYiXFi=ajXFj=bFi=a
9 simpr φaYbYiXFi=ajXFj=bFj=b
10 8 9 oveq12d φaYbYiXFi=ajXFj=bFi˙Fj=a˙b
11 simp-5l φaYbYiXFi=ajXFj=bφ
12 11 1 syl3an1 φaYbYiXFi=ajXFj=bxXyXFx+˙y=Fx˙Fy
13 simp-4r φaYbYiXFi=ajXFj=biX
14 simplr φaYbYiXFi=ajXFj=bjX
15 12 13 14 mhmlem φaYbYiXFi=ajXFj=bFi+˙j=Fi˙Fj
16 fof F:XontoYF:XY
17 6 16 syl φF:XY
18 17 ad5antr φaYbYiXFi=ajXFj=bF:XY
19 7 ad5antr φaYbYiXFi=ajXFj=bGMnd
20 2 4 mndcl GMndiXjXi+˙jX
21 19 13 14 20 syl3anc φaYbYiXFi=ajXFj=bi+˙jX
22 18 21 ffvelrnd φaYbYiXFi=ajXFj=bFi+˙jY
23 15 22 eqeltrrd φaYbYiXFi=ajXFj=bFi˙FjY
24 10 23 eqeltrrd φaYbYiXFi=ajXFj=ba˙bY
25 simpr aYbYbY
26 foelrni F:XontoYbYjXFj=b
27 6 25 26 syl2an φaYbYjXFj=b
28 27 ad2antrr φaYbYiXFi=ajXFj=b
29 24 28 r19.29a φaYbYiXFi=aa˙bY
30 simpl aYbYaY
31 foelrni F:XontoYaYiXFi=a
32 6 30 31 syl2an φaYbYiXFi=a
33 29 32 r19.29a φaYbYa˙bY
34 simpll φaYbYcYφ
35 simplrl φaYbYcYaY
36 simplrr φaYbYcYbY
37 simpr φaYbYcYcY
38 7 ad2antrr φaYbYcYiXGMnd
39 38 ad5antr φaYbYcYiXFi=ajXFj=bkXFk=cGMnd
40 simp-6r φaYbYcYiXFi=ajXFj=bkXFk=ciX
41 simp-4r φaYbYcYiXFi=ajXFj=bkXFk=cjX
42 simplr φaYbYcYiXFi=ajXFj=bkXFk=ckX
43 2 4 mndass GMndiXjXkXi+˙j+˙k=i+˙j+˙k
44 39 40 41 42 43 syl13anc φaYbYcYiXFi=ajXFj=bkXFk=ci+˙j+˙k=i+˙j+˙k
45 44 fveq2d φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j+˙k=Fi+˙j+˙k
46 simp-7l φaYbYcYiXFi=ajXFj=bkXFk=cφ
47 46 1 syl3an1 φaYbYcYiXFi=ajXFj=bkXFk=cxXyXFx+˙y=Fx˙Fy
48 39 40 41 20 syl3anc φaYbYcYiXFi=ajXFj=bkXFk=ci+˙jX
49 47 48 42 mhmlem φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j+˙k=Fi+˙j˙Fk
50 2 4 mndcl GMndjXkXj+˙kX
51 39 41 42 50 syl3anc φaYbYcYiXFi=ajXFj=bkXFk=cj+˙kX
52 47 40 51 mhmlem φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j+˙k=Fi˙Fj+˙k
53 45 49 52 3eqtr3d φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j˙Fk=Fi˙Fj+˙k
54 simp1 φiXjXφ
55 54 1 syl3an1 φiXjXxXyXFx+˙y=Fx˙Fy
56 simp2 φiXjXiX
57 simp3 φiXjXjX
58 55 56 57 mhmlem φiXjXFi+˙j=Fi˙Fj
59 46 40 41 58 syl3anc φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j=Fi˙Fj
60 59 oveq1d φaYbYcYiXFi=ajXFj=bkXFk=cFi+˙j˙Fk=Fi˙Fj˙Fk
61 47 41 42 mhmlem φaYbYcYiXFi=ajXFj=bkXFk=cFj+˙k=Fj˙Fk
62 61 oveq2d φaYbYcYiXFi=ajXFj=bkXFk=cFi˙Fj+˙k=Fi˙Fj˙Fk
63 53 60 62 3eqtr3d φaYbYcYiXFi=ajXFj=bkXFk=cFi˙Fj˙Fk=Fi˙Fj˙Fk
64 simp-5r φaYbYcYiXFi=ajXFj=bkXFk=cFi=a
65 simpllr φaYbYcYiXFi=ajXFj=bkXFk=cFj=b
66 64 65 oveq12d φaYbYcYiXFi=ajXFj=bkXFk=cFi˙Fj=a˙b
67 simpr φaYbYcYiXFi=ajXFj=bkXFk=cFk=c
68 66 67 oveq12d φaYbYcYiXFi=ajXFj=bkXFk=cFi˙Fj˙Fk=a˙b˙c
69 65 67 oveq12d φaYbYcYiXFi=ajXFj=bkXFk=cFj˙Fk=b˙c
70 64 69 oveq12d φaYbYcYiXFi=ajXFj=bkXFk=cFi˙Fj˙Fk=a˙b˙c
71 63 68 70 3eqtr3d φaYbYcYiXFi=ajXFj=bkXFk=ca˙b˙c=a˙b˙c
72 foelrni F:XontoYcYkXFk=c
73 6 72 sylan φcYkXFk=c
74 73 3ad2antr3 φaYbYcYkXFk=c
75 74 ad4antr φaYbYcYiXFi=ajXFj=bkXFk=c
76 71 75 r19.29a φaYbYcYiXFi=ajXFj=ba˙b˙c=a˙b˙c
77 27 3adantr3 φaYbYcYjXFj=b
78 77 ad2antrr φaYbYcYiXFi=ajXFj=b
79 76 78 r19.29a φaYbYcYiXFi=aa˙b˙c=a˙b˙c
80 32 3adantr3 φaYbYcYiXFi=a
81 79 80 r19.29a φaYbYcYa˙b˙c=a˙b˙c
82 34 35 36 37 81 syl13anc φaYbYcYa˙b˙c=a˙b˙c
83 82 ralrimiva φaYbYcYa˙b˙c=a˙b˙c
84 33 83 jca φaYbYa˙bYcYa˙b˙c=a˙b˙c
85 84 ralrimivva φaYbYa˙bYcYa˙b˙c=a˙b˙c
86 eqid 0G=0G
87 2 86 mndidcl GMnd0GX
88 7 87 syl φ0GX
89 17 88 ffvelrnd φF0GY
90 simplll φaYiXFi=aφ
91 90 1 syl3an1 φaYiXFi=axXyXFx+˙y=Fx˙Fy
92 7 ad3antrrr φaYiXFi=aGMnd
93 92 87 syl φaYiXFi=a0GX
94 simplr φaYiXFi=aiX
95 91 93 94 mhmlem φaYiXFi=aF0G+˙i=F0G˙Fi
96 2 4 86 mndlid GMndiX0G+˙i=i
97 92 94 96 syl2anc φaYiXFi=a0G+˙i=i
98 97 fveq2d φaYiXFi=aF0G+˙i=Fi
99 95 98 eqtr3d φaYiXFi=aF0G˙Fi=Fi
100 simpr φaYiXFi=aFi=a
101 100 oveq2d φaYiXFi=aF0G˙Fi=F0G˙a
102 99 101 100 3eqtr3d φaYiXFi=aF0G˙a=a
103 91 94 93 mhmlem φaYiXFi=aFi+˙0G=Fi˙F0G
104 2 4 86 mndrid GMndiXi+˙0G=i
105 92 94 104 syl2anc φaYiXFi=ai+˙0G=i
106 105 fveq2d φaYiXFi=aFi+˙0G=Fi
107 103 106 eqtr3d φaYiXFi=aFi˙F0G=Fi
108 100 oveq1d φaYiXFi=aFi˙F0G=a˙F0G
109 107 108 100 3eqtr3d φaYiXFi=aa˙F0G=a
110 102 109 jca φaYiXFi=aF0G˙a=aa˙F0G=a
111 6 31 sylan φaYiXFi=a
112 110 111 r19.29a φaYF0G˙a=aa˙F0G=a
113 112 ralrimiva φaYF0G˙a=aa˙F0G=a
114 oveq1 d=F0Gd˙a=F0G˙a
115 114 eqeq1d d=F0Gd˙a=aF0G˙a=a
116 115 ovanraleqv d=F0GaYd˙a=aa˙d=aaYF0G˙a=aa˙F0G=a
117 116 rspcev F0GYaYF0G˙a=aa˙F0G=adYaYd˙a=aa˙d=a
118 89 113 117 syl2anc φdYaYd˙a=aa˙d=a
119 3 5 ismnd HMndaYbYa˙bYcYa˙b˙c=a˙b˙cdYaYd˙a=aa˙d=a
120 85 118 119 sylanbrc φHMnd