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

Metamath Proof Explorer

Theorem mgmhmf

Description: A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 mgmhmf.b ⊢ B = Base S
2 mgmhmf.c ⊢ C = Base T
3 eqid ⊢ + S = + S
4 eqid ⊢ + T = + T
5 1 2 3 4 ismgmhm ⊢ F ∈ S MgmHom T ↔ S ∈ Mgm ∧ T ∈ Mgm ∧ F : B ⟶ C ∧ ∀ x ∈ B ∀ y ∈ B F ⁡ x + S y = F ⁡ x + T F ⁡ y
6 simprl ⊢ S ∈ Mgm ∧ T ∈ Mgm ∧ F : B ⟶ C ∧ ∀ x ∈ B ∀ y ∈ B F ⁡ x + S y = F ⁡ x + T F ⁡ y → F : B ⟶ C
7 5 6 sylbi ⊢ F ∈ S MgmHom T → F : B ⟶ C