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

Metamath Proof Explorer

Theorem mhmf

Description: A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses mhmf.b ⊢ B = Base S
mhmf.c ⊢ C = Base T
Assertion mhmf ⊢ F ∈ S MndHom T → F : B ⟶ C

Proof

Step Hyp Ref Expression
1 mhmf.b ⊢ B = Base S
2 mhmf.c ⊢ C = Base T
3 eqid ⊢ + S = + S
4 eqid ⊢ + T = + T
5 eqid ⊢ 0 S = 0 S
6 eqid ⊢ 0 T = 0 T
7 1 2 3 4 5 6 ismhm ⊢ F ∈ S MndHom T ↔ S ∈ Mnd ∧ T ∈ Mnd ∧ F : B ⟶ C ∧ ∀ x ∈ B ∀ y ∈ B F ⁡ x + S y = F ⁡ x + T F ⁡ y ∧ F ⁡ 0 S = 0 T
8 7 simprbi ⊢ F ∈ S MndHom T → F : B ⟶ C ∧ ∀ x ∈ B ∀ y ∈ B F ⁡ x + S y = F ⁡ x + T F ⁡ y ∧ F ⁡ 0 S = 0 T
9 8 simp1d ⊢ F ∈ S MndHom T → F : B ⟶ C