Metamath Proof Explorer

Theorem mhmismgmhm

Description: Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020)

Ref Expression
Assertion mhmismgmhm ⊢ F ∈ R MndHom S → F ∈ R MgmHom S

Proof

Step Hyp Ref Expression
1 mndmgm ⊢ R ∈ Mnd → R ∈ Mgm
2 mndmgm ⊢ S ∈ Mnd → S ∈ Mgm
3 1 2 anim12i ⊢ R ∈ Mnd ∧ S ∈ Mnd → R ∈ Mgm ∧ S ∈ Mgm
4 3simpa ⊢ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y ∧ F ⁡ 0 R = 0 S → F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y
5 3 4 anim12i ⊢ R ∈ Mnd ∧ S ∈ Mnd ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y ∧ F ⁡ 0 R = 0 S → R ∈ Mgm ∧ S ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y
6 eqid ⊢ Base R = Base R
7 eqid ⊢ Base S = Base S
8 eqid ⊢ + R = + R
9 eqid ⊢ + S = + S
10 eqid ⊢ 0 R = 0 R
11 eqid ⊢ 0 S = 0 S
12 6 7 8 9 10 11 ismhm ⊢ F ∈ R MndHom S ↔ R ∈ Mnd ∧ S ∈ Mnd ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y ∧ F ⁡ 0 R = 0 S
13 6 7 8 9 ismgmhm ⊢ F ∈ R MgmHom S ↔ R ∈ Mgm ∧ S ∈ Mgm ∧ F : Base R ⟶ Base S ∧ ∀ x ∈ Base R ∀ y ∈ Base R F ⁡ x + R y = F ⁡ x + S F ⁡ y
14 5 12 13 3imtr4i ⊢ F ∈ R MndHom S → F ∈ R MgmHom S