ismhmd

	Ref	Expression
Hypotheses	ismhmd.b	$⊢ B = {Base}_{S}$
	ismhmd.c	$⊢ C = {Base}_{T}$
	ismhmd.p	$⊢ \underset{˙}{+} = +_{S}$
	ismhmd.q	$⊢ \underset{˙}{⨣} = +_{T}$
	ismhmd.0	$⊢ \underset{˙}{0} = 0_{S}$
	ismhmd.z	$⊢ Z = 0_{T}$
	ismhmd.s	$⊢ φ \to S \in Mnd$
	ismhmd.t	$⊢ φ \to T \in Mnd$
	ismhmd.f	$⊢ φ \to F : B ⟶ C$
	ismhmd.a	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
	ismhmd.h	$⊢ φ \to F (\underset{˙}{0}) = Z$
Assertion	ismhmd	$⊢ φ \to F \in (S MndHom T)$

Step	Hyp	Ref	Expression
1		ismhmd.b	$⊢ B = {Base}_{S}$
2		ismhmd.c	$⊢ C = {Base}_{T}$
3		ismhmd.p	$⊢ \underset{˙}{+} = +_{S}$
4		ismhmd.q	$⊢ \underset{˙}{⨣} = +_{T}$
5		ismhmd.0	$⊢ \underset{˙}{0} = 0_{S}$
6		ismhmd.z	$⊢ Z = 0_{T}$
7		ismhmd.s	$⊢ φ \to S \in Mnd$
8		ismhmd.t	$⊢ φ \to T \in Mnd$
9		ismhmd.f	$⊢ φ \to F : B ⟶ C$
10		ismhmd.a	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
11		ismhmd.h	$⊢ φ \to F (\underset{˙}{0}) = Z$
12	10	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
13	9 12 11	3jca	$⊢ φ \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}) = Z)$
14	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}) = Z))$
15	7 8 13 14	syl21anbrc	$⊢ φ \to F \in (S MndHom T)$

Metamath Proof Explorer