mhmismgmhm

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

		Ref	Expression
	Assertion	mhmismgmhm	$⊢ F \in (R MndHom S) \to F \in (R MgmHom S)$

Step	Hyp	Ref	Expression
1		mndmgm	$⊢ R \in Mnd \to R \in Mgm$
2		mndmgm	$⊢ S \in Mnd \to S \in Mgm$
3	1 2	anim12i	$⊢ (R \in Mnd \land S \in Mnd) \to (R \in Mgm \land S \in Mgm)$
4		3simpa	$⊢ (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y) \land F (0_{R}) = 0_{S}) \to (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y))$
5	3 4	anim12i	$⊢ ((R \in Mnd \land S \in Mnd) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y) \land F (0_{R}) = 0_{S})) \to ((R \in Mgm \land S \in Mgm) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {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 \in (R MndHom S) \leftrightarrow ((R \in Mnd \land S \in Mnd) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y) \land F (0_{R}) = 0_{S}))$
13	6 7 8 9	ismgmhm	$⊢ F \in (R MgmHom S) \leftrightarrow ((R \in Mgm \land S \in Mgm) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y)))$
14	5 12 13	3imtr4i	$⊢ F \in (R MndHom S) \to F \in (R MgmHom S)$

Metamath Proof Explorer