Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gsmhom Unicode version

Definition df-gsmhom 25491
Description: Define the set of semigroup homomorphisms from  g to  h. Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-gsmhom  |-  SemiGrpHom  =  (
g  e.  SemiGrp ,  h  e.  SemiGrp  |->  { f  |  ( f : dom  dom  g --> dom  dom  h  /\  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( f `
 x ) h ( f `  y
) )  =  ( f `  ( x g y ) ) ) } )
Distinct variable group:    f, g, h, x, y

Detailed syntax breakdown of Definition df-gsmhom
StepHypRef Expression
1 csmhom 25490 . 2  class  SemiGrpHom
2 vg . . 3  set  g
3 vh . . 3  set  h
4 csem 21013 . . 3  class  SemiGrp
52cv 1631 . . . . . . . 8  class  g
65cdm 4705 . . . . . . 7  class  dom  g
76cdm 4705 . . . . . 6  class  dom  dom  g
83cv 1631 . . . . . . . 8  class  h
98cdm 4705 . . . . . . 7  class  dom  h
109cdm 4705 . . . . . 6  class  dom  dom  h
11 vf . . . . . . 7  set  f
1211cv 1631 . . . . . 6  class  f
137, 10, 12wf 5267 . . . . 5  wff  f : dom  dom  g --> dom  dom  h
14 vx . . . . . . . . . . 11  set  x
1514cv 1631 . . . . . . . . . 10  class  x
1615, 12cfv 5271 . . . . . . . . 9  class  ( f `
 x )
17 vy . . . . . . . . . . 11  set  y
1817cv 1631 . . . . . . . . . 10  class  y
1918, 12cfv 5271 . . . . . . . . 9  class  ( f `
 y )
2016, 19, 8co 5874 . . . . . . . 8  class  ( ( f `  x ) h ( f `  y ) )
2115, 18, 5co 5874 . . . . . . . . 9  class  ( x g y )
2221, 12cfv 5271 . . . . . . . 8  class  ( f `
 ( x g y ) )
2320, 22wceq 1632 . . . . . . 7  wff  ( ( f `  x ) h ( f `  y ) )  =  ( f `  (
x g y ) )
2423, 17, 7wral 2556 . . . . . 6  wff  A. y  e.  dom  dom  g (
( f `  x
) h ( f `
 y ) )  =  ( f `  ( x g y ) )
2524, 14, 7wral 2556 . . . . 5  wff  A. x  e.  dom  dom  g A. y  e.  dom  dom  g
( ( f `  x ) h ( f `  y ) )  =  ( f `
 ( x g y ) )
2613, 25wa 358 . . . 4  wff  ( f : dom  dom  g --> dom  dom  h  /\  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( f `
 x ) h ( f `  y
) )  =  ( f `  ( x g y ) ) )
2726, 11cab 2282 . . 3  class  { f  |  ( f : dom  dom  g --> dom  dom  h  /\  A. x  e. 
dom  dom  g A. y  e.  dom  dom  g (
( f `  x
) h ( f `
 y ) )  =  ( f `  ( x g y ) ) ) }
282, 3, 4, 4, 27cmpt2 5876 . 2  class  ( g  e.  SemiGrp ,  h  e.  SemiGrp 
|->  { f  |  ( f : dom  dom  g
--> dom  dom  h  /\  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( f `
 x ) h ( f `  y
) )  =  ( f `  ( x g y ) ) ) } )
291, 28wceq 1632 1  wff  SemiGrpHom  =  (
g  e.  SemiGrp ,  h  e.  SemiGrp  |->  { f  |  ( f : dom  dom  g --> dom  dom  h  /\  A. x  e.  dom  dom  g A. y  e.  dom  dom  g ( ( f `
 x ) h ( f `  y
) )  =  ( f `  ( x g y ) ) ) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator