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 𝑆 ) )