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

Metamath Proof Explorer

Theorem mhmismgmhm

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

Ref Expression
Assertion mhmismgmhm ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) )

Proof

Step Hyp Ref Expression
1 mndmgm ⊢ ( 𝑅 ∈ Mnd → 𝑅 ∈ Mgm )
2 mndmgm ⊢ ( 𝑆 ∈ Mnd → 𝑆 ∈ Mgm )
3 1 2 anim12i ⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) → ( 𝑅 ∈ Mgm ∧ 𝑆 ∈ Mgm ) )
4 3simpa ⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) ) → ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) )
5 3 4 anim12i ⊢ ( ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) ) ) → ( ( 𝑅 ∈ Mgm ∧ 𝑆 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
9 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
10 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
12 6 7 8 9 10 11 ismhm ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ↔ ( ( 𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) ) ) )
13 6 7 8 9 ismgmhm ⊢ ( 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) ↔ ( ( 𝑅 ∈ Mgm ∧ 𝑆 ∈ Mgm ) ∧ ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
14 5 12 13 3imtr4i ⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MgmHom 𝑆 ) )