Description: The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | mhmco | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mhmrcl2 | |
|
2 | mhmrcl1 | |
|
3 | 1 2 | anim12ci | |
4 | eqid | |
|
5 | eqid | |
|
6 | 4 5 | mhmf | |
7 | eqid | |
|
8 | 7 4 | mhmf | |
9 | fco | |
|
10 | 6 8 9 | syl2an | |
11 | eqid | |
|
12 | eqid | |
|
13 | 7 11 12 | mhmlin | |
14 | 13 | 3expb | |
15 | 14 | adantll | |
16 | 15 | fveq2d | |
17 | simpll | |
|
18 | 8 | ad2antlr | |
19 | simprl | |
|
20 | 18 19 | ffvelcdmd | |
21 | simprr | |
|
22 | 18 21 | ffvelcdmd | |
23 | eqid | |
|
24 | 4 12 23 | mhmlin | |
25 | 17 20 22 24 | syl3anc | |
26 | 16 25 | eqtrd | |
27 | 2 | adantl | |
28 | 7 11 | mndcl | |
29 | 28 | 3expb | |
30 | 27 29 | sylan | |
31 | fvco3 | |
|
32 | 18 30 31 | syl2anc | |
33 | fvco3 | |
|
34 | 18 19 33 | syl2anc | |
35 | fvco3 | |
|
36 | 18 21 35 | syl2anc | |
37 | 34 36 | oveq12d | |
38 | 26 32 37 | 3eqtr4d | |
39 | 38 | ralrimivva | |
40 | 8 | adantl | |
41 | eqid | |
|
42 | 7 41 | mndidcl | |
43 | 27 42 | syl | |
44 | fvco3 | |
|
45 | 40 43 44 | syl2anc | |
46 | eqid | |
|
47 | 41 46 | mhm0 | |
48 | 47 | adantl | |
49 | 48 | fveq2d | |
50 | eqid | |
|
51 | 46 50 | mhm0 | |
52 | 51 | adantr | |
53 | 45 49 52 | 3eqtrd | |
54 | 10 39 53 | 3jca | |
55 | 7 5 11 23 41 50 | ismhm | |
56 | 3 54 55 | sylanbrc | |