Theorem ghmco

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

	Ref	Expression
Assertion	ghmco	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		ghmmhm	⊢ ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) → 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) )
2		ghmmhm	⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) )
3		mhmco	⊢ ( ( 𝐹 ∈ ( 𝑇 MndHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MndHom 𝑈 ) )
4	1 2 3	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 MndHom 𝑈 ) )
5		ghmgrp1	⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
6		ghmgrp2	⊢ ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) → 𝑈 ∈ Grp )
7		ghmmhmb	⊢ ( ( 𝑆 ∈ Grp ∧ 𝑈 ∈ Grp ) → ( 𝑆 GrpHom 𝑈 ) = ( 𝑆 MndHom 𝑈 ) )
8	5 6 7	syl2anr	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑆 GrpHom 𝑈 ) = ( 𝑆 MndHom 𝑈 ) )
9	4 8	eleqtrrd	⊢ ( ( 𝐹 ∈ ( 𝑇 GrpHom 𝑈 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑆 GrpHom 𝑈 ) )