ghmco

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

		Ref	Expression
	Assertion	ghmco	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$

Step	Hyp	Ref	Expression
1		ghmmhm	$⊢ F \in (T GrpHom U) \to F \in (T MndHom U)$
2		ghmmhm	$⊢ G \in (S GrpHom T) \to G \in (S MndHom T)$
3		mhmco	$⊢ (F \in (T MndHom U) \land G \in (S MndHom T)) \to F \circ G \in (S MndHom U)$
4	1 2 3	syl2an	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S MndHom U)$
5		ghmgrp1	$⊢ G \in (S GrpHom T) \to S \in Grp$
6		ghmgrp2	$⊢ F \in (T GrpHom U) \to U \in Grp$
7		ghmmhmb	$⊢ (S \in Grp \land U \in Grp) \to S GrpHom U = S MndHom U$
8	5 6 7	syl2anr	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to S GrpHom U = S MndHom U$
9	4 8	eleqtrrd	$⊢ (F \in (T GrpHom U) \land G \in (S GrpHom T)) \to F \circ G \in (S GrpHom U)$

Metamath Proof Explorer