This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ ( 𝑇 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 𝑈 ) )