This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )