Metamath Proof Explorer

Definition df-ghomOLD

Description: Obsolete version of df-ghm as of 15-Mar-2020. Define the set of group homomorphisms from g to h . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

Ref Expression
Assertion df-ghomOLD 
|- GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cghomOLD 
 |-  GrpOpHom
1 vg 
 |-  g
2 cgr 
 |-  GrpOp
3 vh 
 |-  h
4 vf 
 |-  f
5 4 cv 
 |-  f
6 1 cv 
 |-  g
7 6 crn 
 |-  ran g
8 3 cv 
 |-  h
9 8 crn 
 |-  ran h
10 7 9 5 wf 
 |-  f : ran g --> ran h
11 vx 
 |-  x
12 vy 
 |-  y
13 11 cv 
 |-  x
14 13 5 cfv 
 |-  ( f ` x )
15 12 cv 
 |-  y
16 15 5 cfv 
 |-  ( f ` y )
17 14 16 8 co 
 |-  ( ( f ` x ) h ( f ` y ) )
18 13 15 6 co 
 |-  ( x g y )
19 18 5 cfv 
 |-  ( f ` ( x g y ) )
20 17 19 wceq 
 |-  ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
21 20 12 7 wral 
 |-  A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
22 21 11 7 wral 
 |-  A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) )
23 10 22 wa 
 |-  ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) )
24 23 4 cab 
 |-  { 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 ) ) ) }
25 1 3 2 2 24 cmpo 
 |-  ( g e. GrpOp , h e. GrpOp |-> { 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 ) ) ) } )
26 0 25 wceq 
 |-  GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { 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 ) ) ) } )