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

Definition df-ghom 21041
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 21040 . 2  class GrpOpHom
2 vg . . 3  set  g
3 vh . . 3  set  h
4 cgr 20869 . . 3  class  GrpOp
52cv 1631 . . . . . . 7  class  g
65crn 4706 . . . . . 6  class  ran  g
73cv 1631 . . . . . . 7  class  h
87crn 4706 . . . . . 6  class  ran  h
9 vf . . . . . . 7  set  f
109cv 1631 . . . . . 6  class  f
116, 8, 10wf 5267 . . . . 5  wff  f : ran  g --> ran  h
12 vx . . . . . . . . . . 11  set  x
1312cv 1631 . . . . . . . . . 10  class  x
1413, 10cfv 5271 . . . . . . . . 9  class  ( f `
 x )
15 vy . . . . . . . . . . 11  set  y
1615cv 1631 . . . . . . . . . 10  class  y
1716, 10cfv 5271 . . . . . . . . 9  class  ( f `
 y )
1814, 17, 7co 5874 . . . . . . . 8  class  ( ( f `  x ) h ( f `  y ) )
1913, 16, 5co 5874 . . . . . . . . 9  class  ( x g y )
2019, 10cfv 5271 . . . . . . . 8  class  ( f `
 ( x g y ) )
2118, 20wceq 1632 . . . . . . 7  wff  ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2221, 15, 6wral 2556 . . . . . 6  wff  A. y  e.  ran  g ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2322, 12, 6wral 2556 . . . . 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 2282 . . 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 5876 . 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 1632 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  21044
  Copyright terms: Public domain W3C validator