Theorem 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	|- .+ = ( +g ` S )
	isghmd.b	|- .+^ = ( +g ` T )
	isghmd.s	|- ( ph -> S e. Grp )
	isghmd.t	|- ( ph -> T e. Grp )
	isghmd.f	|- ( ph -> F : X --> Y )
	isghmd.l	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
Assertion	isghmd	|- ( ph -> F e. ( S GrpHom T ) )

Proof

Step	Hyp	Ref	Expression
1		isghmd.x	|- X = ( Base ` S )
2		isghmd.y	|- Y = ( Base ` T )
3		isghmd.a	|- .+ = ( +g ` S )
4		isghmd.b	|- .+^ = ( +g ` T )
5		isghmd.s	|- ( ph -> S e. Grp )
6		isghmd.t	|- ( ph -> T e. Grp )
7		isghmd.f	|- ( ph -> F : X --> Y )
8		isghmd.l	|- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
9	8	ralrimivva	|- ( ph -> A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
10	7 9	jca	|- ( ph -> ( F : X --> Y /\ A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
11	1 2 3 4	isghm	|- ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. x e. X A. y e. X ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) ) )
12	5 6 10 11	syl21anbrc	|- ( ph -> F e. ( S GrpHom T ) )