Metamath Proof Explorer

Theorem mhmco

Description: The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Assertion mhmco 
|- ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )

Proof

Step Hyp Ref Expression
1 mhmrcl2 
 |-  ( F e. ( T MndHom U ) -> U e. Mnd )
2 mhmrcl1 
 |-  ( G e. ( S MndHom T ) -> S e. Mnd )
3 1 2 anim12ci 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( S e. Mnd /\ U e. Mnd ) )
4 eqid 
 |-  ( Base ` T ) = ( Base ` T )
5 eqid 
 |-  ( Base ` U ) = ( Base ` U )
6 4 5 mhmf 
 |-  ( F e. ( T MndHom U ) -> F : ( Base ` T ) --> ( Base ` U ) )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 7 4 mhmf 
 |-  ( G e. ( S MndHom T ) -> G : ( Base ` S ) --> ( Base ` T ) )
9 fco 
 |-  ( ( F : ( Base ` T ) --> ( Base ` U ) /\ G : ( Base ` S ) --> ( Base ` T ) ) -> ( F o. G ) : ( Base ` S ) --> ( Base ` U ) )
10 6 8 9 syl2an 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) : ( Base ` S ) --> ( Base ` U ) )
11 eqid 
 |-  ( +g ` S ) = ( +g ` S )
12 eqid 
 |-  ( +g ` T ) = ( +g ` T )
13 7 11 12 mhmlin 
 |-  ( ( G e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
14 13 3expb 
 |-  ( ( G e. ( S MndHom T ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
15 14 adantll 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( G ` ( x ( +g ` S ) y ) ) = ( ( G ` x ) ( +g ` T ) ( G ` y ) ) )
16 15 fveq2d 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( G ` ( x ( +g ` S ) y ) ) ) = ( F ` ( ( G ` x ) ( +g ` T ) ( G ` y ) ) ) )
17 simpll 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> F e. ( T MndHom U ) )
18 8 ad2antlr 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
19 simprl 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
20 18 19 ffvelrnd 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( G ` x ) e. ( Base ` T ) )
21 simprr 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
22 18 21 ffvelrnd 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( G ` y ) e. ( Base ` T ) )
23 eqid 
 |-  ( +g ` U ) = ( +g ` U )
24 4 12 23 mhmlin 
 |-  ( ( F e. ( T MndHom U ) /\ ( G ` x ) e. ( Base ` T ) /\ ( G ` y ) e. ( Base ` T ) ) -> ( F ` ( ( G ` x ) ( +g ` T ) ( G ` y ) ) ) = ( ( F ` ( G ` x ) ) ( +g ` U ) ( F ` ( G ` y ) ) ) )
25 17 20 22 24 syl3anc 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( ( G ` x ) ( +g ` T ) ( G ` y ) ) ) = ( ( F ` ( G ` x ) ) ( +g ` U ) ( F ` ( G ` y ) ) ) )
26 16 25 eqtrd 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( G ` ( x ( +g ` S ) y ) ) ) = ( ( F ` ( G ` x ) ) ( +g ` U ) ( F ` ( G ` y ) ) ) )
27 2 adantl 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> S e. Mnd )
28 7 11 mndcl 
 |-  ( ( S e. Mnd /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
29 28 3expb 
 |-  ( ( S e. Mnd /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
30 27 29 sylan 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
31 fvco3 
 |-  ( ( G : ( Base ` S ) --> ( Base ` T ) /\ ( x ( +g ` S ) y ) e. ( Base ` S ) ) -> ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( F ` ( G ` ( x ( +g ` S ) y ) ) ) )
32 18 30 31 syl2anc 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( F ` ( G ` ( x ( +g ` S ) y ) ) ) )
33 fvco3 
 |-  ( ( G : ( Base ` S ) --> ( Base ` T ) /\ x e. ( Base ` S ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
34 18 19 33 syl2anc 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
35 fvco3 
 |-  ( ( G : ( Base ` S ) --> ( Base ` T ) /\ y e. ( Base ` S ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
36 18 21 35 syl2anc 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F o. G ) ` y ) = ( F ` ( G ` y ) ) )
37 34 36 oveq12d 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( ( F o. G ) ` x ) ( +g ` U ) ( ( F o. G ) ` y ) ) = ( ( F ` ( G ` x ) ) ( +g ` U ) ( F ` ( G ` y ) ) ) )
38 26 32 37 3eqtr4d 
 |-  ( ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( ( ( F o. G ) ` x ) ( +g ` U ) ( ( F o. G ) ` y ) ) )
39 38 ralrimivva 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( ( ( F o. G ) ` x ) ( +g ` U ) ( ( F o. G ) ` y ) ) )
40 8 adantl 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> G : ( Base ` S ) --> ( Base ` T ) )
41 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
42 7 41 mndidcl 
 |-  ( S e. Mnd -> ( 0g ` S ) e. ( Base ` S ) )
43 27 42 syl 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( 0g ` S ) e. ( Base ` S ) )
44 fvco3 
 |-  ( ( G : ( Base ` S ) --> ( Base ` T ) /\ ( 0g ` S ) e. ( Base ` S ) ) -> ( ( F o. G ) ` ( 0g ` S ) ) = ( F ` ( G ` ( 0g ` S ) ) ) )
45 40 43 44 syl2anc 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( ( F o. G ) ` ( 0g ` S ) ) = ( F ` ( G ` ( 0g ` S ) ) ) )
46 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
47 41 46 mhm0 
 |-  ( G e. ( S MndHom T ) -> ( G ` ( 0g ` S ) ) = ( 0g ` T ) )
48 47 adantl 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( G ` ( 0g ` S ) ) = ( 0g ` T ) )
49 48 fveq2d 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F ` ( G ` ( 0g ` S ) ) ) = ( F ` ( 0g ` T ) ) )
50 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
51 46 50 mhm0 
 |-  ( F e. ( T MndHom U ) -> ( F ` ( 0g ` T ) ) = ( 0g ` U ) )
52 51 adantr 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F ` ( 0g ` T ) ) = ( 0g ` U ) )
53 45 49 52 3eqtrd 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( ( F o. G ) ` ( 0g ` S ) ) = ( 0g ` U ) )
54 10 39 53 3jca 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( ( F o. G ) : ( Base ` S ) --> ( Base ` U ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( ( ( F o. G ) ` x ) ( +g ` U ) ( ( F o. G ) ` y ) ) /\ ( ( F o. G ) ` ( 0g ` S ) ) = ( 0g ` U ) ) )
55 7 5 11 23 41 50 ismhm 
 |-  ( ( F o. G ) e. ( S MndHom U ) <-> ( ( S e. Mnd /\ U e. Mnd ) /\ ( ( F o. G ) : ( Base ` S ) --> ( Base ` U ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( ( F o. G ) ` ( x ( +g ` S ) y ) ) = ( ( ( F o. G ) ` x ) ( +g ` U ) ( ( F o. G ) ` y ) ) /\ ( ( F o. G ) ` ( 0g ` S ) ) = ( 0g ` U ) ) ) )
56 3 54 55 sylanbrc 
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )