Metamath Proof Explorer

Theorem ismhm0

Description: Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020)

		Ref	Expression
	Hypotheses	ismhm0.b	$⊢ B = {Base}_{S}$
		ismhm0.c	$⊢ C = {Base}_{T}$
		ismhm0.p	$⊢ \underset{˙}{+} = +_{S}$
		ismhm0.q	$⊢ \underset{˙}{⨣} = +_{T}$
		ismhm0.z	$⊢ \underset{˙}{0} = 0_{S}$
		ismhm0.y	$⊢ Y = 0_{T}$
	Assertion	ismhm0	$⊢ F \in (S MndHom T) \leftrightarrow ((S \in Mnd \land T \in Mnd) \land (F \in (S MgmHom T) \land F (\underset{˙}{0}) = Y))$

Proof

Step	Hyp	Ref	Expression
1		ismhm0.b	$⊢ B = {Base}_{S}$
2		ismhm0.c	$⊢ C = {Base}_{T}$
3		ismhm0.p	$⊢ \underset{˙}{+} = +_{S}$
4		ismhm0.q	$⊢ \underset{˙}{⨣} = +_{T}$
5		ismhm0.z	$⊢ \underset{˙}{0} = 0_{S}$
6		ismhm0.y	$⊢ Y = 0_{T}$
7	1 2 3 4 5 6	ismhm	$⊢ F \in (S MndHom T) \leftrightarrow ((S \in Mnd \land T \in Mnd) \land (F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (\underset{˙}{0}) = Y))$
8		df-3an	$⊢ (F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (\underset{˙}{0}) = Y) \leftrightarrow ((F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)) \land F (\underset{˙}{0}) = Y)$
9		mndmgm	$⊢ S \in Mnd \to S \in Mgm$
10		mndmgm	$⊢ T \in Mnd \to T \in Mgm$
11	9 10	anim12i	$⊢ (S \in Mnd \land T \in Mnd) \to (S \in Mgm \land T \in Mgm)$
12	11	biantrurd	$⊢ (S \in Mnd \land T \in Mnd) \to ((F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)) \leftrightarrow ((S \in Mgm \land T \in Mgm) \land (F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y))))$
13	1 2 3 4	ismgmhm	$⊢ F \in (S MgmHom T) \leftrightarrow ((S \in Mgm \land T \in Mgm) \land (F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)))$
14	12 13	bitr4di	$⊢ (S \in Mnd \land T \in Mnd) \to ((F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)) \leftrightarrow F \in (S MgmHom T))$
15	14	anbi1d	$⊢ (S \in Mnd \land T \in Mnd) \to (((F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)) \land F (\underset{˙}{0}) = Y) \leftrightarrow (F \in (S MgmHom T) \land F (\underset{˙}{0}) = Y))$
16	8 15	syl5bb	$⊢ (S \in Mnd \land T \in Mnd) \to ((F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (\underset{˙}{0}) = Y) \leftrightarrow (F \in (S MgmHom T) \land F (\underset{˙}{0}) = Y))$
17	16	pm5.32i	$⊢ ((S \in Mnd \land T \in Mnd) \land (F : B ⟶ C \land \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (\underset{˙}{0}) = Y)) \leftrightarrow ((S \in Mnd \land T \in Mnd) \land (F \in (S MgmHom T) \land F (\underset{˙}{0}) = Y))$
18	7 17	bitri	$⊢ F \in (S MndHom T) \leftrightarrow ((S \in Mnd \land T \in Mnd) \land (F \in (S MgmHom T) \land F (\underset{˙}{0}) = Y))$