isghmd

Description: Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

	Ref	Expression
Hypotheses	isghmd.x	$⊢ X = {Base}_{S}$
	isghmd.y	$⊢ Y = {Base}_{T}$
	isghmd.a	$⊢ \underset{˙}{+} = +_{S}$
	isghmd.b	$⊢ \underset{˙}{⨣} = +_{T}$
	isghmd.s	$⊢ φ \to S \in Grp$
	isghmd.t	$⊢ φ \to T \in Grp$
	isghmd.f	$⊢ φ \to F : X ⟶ Y$
	isghmd.l	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
Assertion	isghmd	$⊢ φ \to F \in (S GrpHom T)$

Step	Hyp	Ref	Expression
1		isghmd.x	$⊢ X = {Base}_{S}$
2		isghmd.y	$⊢ Y = {Base}_{T}$
3		isghmd.a	$⊢ \underset{˙}{+} = +_{S}$
4		isghmd.b	$⊢ \underset{˙}{⨣} = +_{T}$
5		isghmd.s	$⊢ φ \to S \in Grp$
6		isghmd.t	$⊢ φ \to T \in Grp$
7		isghmd.f	$⊢ φ \to F : X ⟶ Y$
8		isghmd.l	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
9	8	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
10	7 9	jca	$⊢ φ \to (F : X ⟶ Y \land \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y))$
11	1 2 3 4	isghm	$⊢ F \in (S GrpHom T) \leftrightarrow ((S \in Grp \land T \in Grp) \land (F : X ⟶ Y \land \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)))$
12	5 6 10 11	syl21anbrc	$⊢ φ \to F \in (S GrpHom T)$

Metamath Proof Explorer