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 ) )