MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ghom Unicode version

Definition df-ghom 21025
Description: Define the set of group homomorphisms from  g to  h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-ghom  |- 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 ) ) ) } )
Distinct variable group:    f, g, h, x, y

Detailed syntax breakdown of Definition df-ghom
StepHypRef Expression
1 cghom 21024 . 2  class GrpOpHom
2 vg . . 3  set  g
3 vh . . 3  set  h
4 cgr 20853 . . 3  class  GrpOp
52cv 1622 . . . . . . 7  class  g
65crn 4690 . . . . . 6  class  ran  g
73cv 1622 . . . . . . 7  class  h
87crn 4690 . . . . . 6  class  ran  h
9 vf . . . . . . 7  set  f
109cv 1622 . . . . . 6  class  f
116, 8, 10wf 5251 . . . . 5  wff  f : ran  g --> ran  h
12 vx . . . . . . . . . . 11  set  x
1312cv 1622 . . . . . . . . . 10  class  x
1413, 10cfv 5255 . . . . . . . . 9  class  ( f `
 x )
15 vy . . . . . . . . . . 11  set  y
1615cv 1622 . . . . . . . . . 10  class  y
1716, 10cfv 5255 . . . . . . . . 9  class  ( f `
 y )
1814, 17, 7co 5858 . . . . . . . 8  class  ( ( f `  x ) h ( f `  y ) )
1913, 16, 5co 5858 . . . . . . . . 9  class  ( x g y )
2019, 10cfv 5255 . . . . . . . 8  class  ( f `
 ( x g y ) )
2118, 20wceq 1623 . . . . . . 7  wff  ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2221, 15, 6wral 2543 . . . . . 6  wff  A. y  e.  ran  g ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2322, 12, 6wral 2543 . . . . 5  wff  A. x  e.  ran  g A. y  e.  ran  g ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2411, 23wa 358 . . . 4  wff  ( f : ran  g --> ran  h  /\  A. x  e.  ran  g A. y  e.  ran  g ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) ) )
2524, 9cab 2269 . . 3  class  { 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 ) ) ) }
262, 3, 4, 4, 25cmpt2 5860 . 2  class  ( 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 ) ) ) } )
271, 26wceq 1623 1  wff 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 ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  elghomlem1  21028
  Copyright terms: Public domain W3C validator