Metamath Proof Explorer

Theorem isghm3

Description: Property of a group homomorphism, similar to ismhm . (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses isghm.w 
|- X = ( Base ` S )
isghm.x 
|- Y = ( Base ` T )
isghm.a 
|- .+ = ( +g ` S )
isghm.b 
|- .+^ = ( +g ` T )
Assertion isghm3 
|- ( ( S e. Grp /\ T e. Grp ) -> ( F e. ( S GrpHom T ) <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isghm.w 
 |-  X = ( Base ` S )
2 isghm.x 
 |-  Y = ( Base ` T )
3 isghm.a 
 |-  .+ = ( +g ` S )
4 isghm.b 
 |-  .+^ = ( +g ` T )
5 1 2 3 4 isghm 
 |-  ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )
6 5 baib 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( F e. ( S GrpHom T ) <-> ( F : X --> Y /\ A. u e. X A. v e. X ( F ` ( u .+ v ) ) = ( ( F ` u ) .+^ ( F ` v ) ) ) ) )