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

Metamath Proof Explorer

Theorem ghmf

Description: A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Hypotheses ghmf.x ⊢ X = Base S
ghmf.y ⊢ Y = Base T
Assertion ghmf ⊢ F ∈ S GrpHom T → F : X ⟶ Y

Proof

Step Hyp Ref Expression
1 ghmf.x ⊢ X = Base S
2 ghmf.y ⊢ Y = 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 : X ⟶ Y ∧ ∀ y ∈ X ∀ x ∈ X F ⁡ y + S x = F ⁡ y + T F ⁡ x
6 5 simprbi ⊢ F ∈ S GrpHom T → F : X ⟶ Y ∧ ∀ y ∈ X ∀ x ∈ X F ⁡ y + S x = F ⁡ y + T F ⁡ x
7 6 simpld ⊢ F ∈ S GrpHom T → F : X ⟶ Y