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

Metamath Proof Explorer

Theorem ghmgrp2

Description: A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmgrp2 ⊢ F ∈ S GrpHom T → T ∈ Grp

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base S = Base S
2 eqid ⊢ Base T = Base T
3 eqid ⊢ + S = + S
4 eqid ⊢ + T = + T
5 1 2 3 4 isghm ⊢ F ∈ S GrpHom T ↔ S ∈ Grp ∧ T ∈ Grp ∧ F : Base S ⟶ Base T ∧ ∀ y ∈ Base S ∀ x ∈ Base S F ⁡ y + S x = F ⁡ y + T F ⁡ x
6 5 simplbi ⊢ F ∈ S GrpHom T → S ∈ Grp ∧ T ∈ Grp
7 6 simprd ⊢ F ∈ S GrpHom T → T ∈ Grp