Theorem elghomOLD

Description: Obsolete version of isghm as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H . (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	elghomOLD.1	|- X = ran G
	elghomOLD.2	|- W = ran H
Assertion	elghomOLD	|- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elghomOLD.1	|- X = ran G
2		elghomOLD.2	|- W = ran H
3		eqid	|- { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) } = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }
4	3	elghomlem2OLD	|- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
5	1 2	feq23i	|- ( F : X --> W <-> F : ran G --> ran H )
6	1	raleqi	|- ( A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) <-> A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) )
7	1 6	raleqbii	|- ( A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) <-> A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) )
8	5 7	anbi12i	|- ( ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) )
9	4 8	bitr4di	|- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )