Metamath Proof Explorer


Theorem ghmco

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

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

Proof

Step Hyp Ref Expression
1 ghmmhm
 |-  ( F e. ( T GrpHom U ) -> F e. ( T MndHom U ) )
2 ghmmhm
 |-  ( G e. ( S GrpHom T ) -> G e. ( S MndHom T ) )
3 mhmco
 |-  ( ( F e. ( T MndHom U ) /\ G e. ( S MndHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )
4 1 2 3 syl2an
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S MndHom U ) )
5 ghmgrp1
 |-  ( G e. ( S GrpHom T ) -> S e. Grp )
6 ghmgrp2
 |-  ( F e. ( T GrpHom U ) -> U e. Grp )
7 ghmmhmb
 |-  ( ( S e. Grp /\ U e. Grp ) -> ( S GrpHom U ) = ( S MndHom U ) )
8 5 6 7 syl2anr
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( S GrpHom U ) = ( S MndHom U ) )
9 4 8 eleqtrrd
 |-  ( ( F e. ( T GrpHom U ) /\ G e. ( S GrpHom T ) ) -> ( F o. G ) e. ( S GrpHom U ) )