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

Definition df-ghm 14683
Description: A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Assertion
Ref Expression
df-ghm  |-  GrpHom  =  ( s  e.  Grp , 
t  e.  Grp  |->  { g  |  [. ( Base `  s )  /  w ]. ( g : w --> ( Base `  t
)  /\  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) ) ) } )
Distinct variable group:    g, s, t, w, x, y

Detailed syntax breakdown of Definition df-ghm
StepHypRef Expression
1 cghm 14682 . 2  class  GrpHom
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cgrp 14364 . . 3  class  Grp
5 vw . . . . . . . 8  set  w
65cv 1624 . . . . . . 7  class  w
73cv 1624 . . . . . . . 8  class  t
8 cbs 13150 . . . . . . . 8  class  Base
97, 8cfv 5257 . . . . . . 7  class  ( Base `  t )
10 vg . . . . . . . 8  set  g
1110cv 1624 . . . . . . 7  class  g
126, 9, 11wf 5253 . . . . . 6  wff  g : w --> ( Base `  t
)
13 vx . . . . . . . . . . . 12  set  x
1413cv 1624 . . . . . . . . . . 11  class  x
15 vy . . . . . . . . . . . 12  set  y
1615cv 1624 . . . . . . . . . . 11  class  y
172cv 1624 . . . . . . . . . . . 12  class  s
18 cplusg 13210 . . . . . . . . . . . 12  class  +g
1917, 18cfv 5257 . . . . . . . . . . 11  class  ( +g  `  s )
2014, 16, 19co 5860 . . . . . . . . . 10  class  ( x ( +g  `  s
) y )
2120, 11cfv 5257 . . . . . . . . 9  class  ( g `
 ( x ( +g  `  s ) y ) )
2214, 11cfv 5257 . . . . . . . . . 10  class  ( g `
 x )
2316, 11cfv 5257 . . . . . . . . . 10  class  ( g `
 y )
247, 18cfv 5257 . . . . . . . . . 10  class  ( +g  `  t )
2522, 23, 24co 5860 . . . . . . . . 9  class  ( ( g `  x ) ( +g  `  t
) ( g `  y ) )
2621, 25wceq 1625 . . . . . . . 8  wff  ( g `
 ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t ) ( g `
 y ) )
2726, 15, 6wral 2545 . . . . . . 7  wff  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) )
2827, 13, 6wral 2545 . . . . . 6  wff  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) )
2912, 28wa 358 . . . . 5  wff  ( g : w --> ( Base `  t )  /\  A. x  e.  w  A. y  e.  w  (
g `  ( x
( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t ) ( g `
 y ) ) )
3017, 8cfv 5257 . . . . 5  class  ( Base `  s )
3129, 5, 30wsbc 2993 . . . 4  wff  [. ( Base `  s )  /  w ]. ( g : w --> ( Base `  t
)  /\  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) ) )
3231, 10cab 2271 . . 3  class  { g  |  [. ( Base `  s )  /  w ]. ( g : w --> ( Base `  t
)  /\  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) ) ) }
332, 3, 4, 4, 32cmpt2 5862 . 2  class  ( s  e.  Grp ,  t  e.  Grp  |->  { g  |  [. ( Base `  s )  /  w ]. ( g : w --> ( Base `  t
)  /\  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) ) ) } )
341, 33wceq 1625 1  wff  GrpHom  =  ( s  e.  Grp , 
t  e.  Grp  |->  { g  |  [. ( Base `  s )  /  w ]. ( g : w --> ( Base `  t
)  /\  A. x  e.  w  A. y  e.  w  ( g `  ( x ( +g  `  s ) y ) )  =  ( ( g `  x ) ( +g  `  t
) ( g `  y ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  reldmghm  14684  isghm  14685
  Copyright terms: Public domain W3C validator