This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ghm

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)

Ref Expression
Assertion 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 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cghm 
 |-  GrpHom
1 vs 
 |-  s
2 cgrp 
 |-  Grp
3 vt 
 |-  t
4 vg 
 |-  g
5 cbs 
 |-  Base
6 1 cv 
 |-  s
7 6 5 cfv 
 |-  ( Base ` s )
8 vw 
 |-  w
9 4 cv 
 |-  g
10 8 cv 
 |-  w
11 3 cv 
 |-  t
12 11 5 cfv 
 |-  ( Base ` t )
13 10 12 9 wf 
 |-  g : w --> ( Base ` t )
14 vx 
 |-  x
15 vy 
 |-  y
16 14 cv 
 |-  x
17 cplusg 
 |-  +g
18 6 17 cfv 
 |-  ( +g ` s )
19 15 cv 
 |-  y
20 16 19 18 co 
 |-  ( x ( +g ` s ) y )
21 20 9 cfv 
 |-  ( g ` ( x ( +g ` s ) y ) )
22 16 9 cfv 
 |-  ( g ` x )
23 11 17 cfv 
 |-  ( +g ` t )
24 19 9 cfv 
 |-  ( g ` y )
25 22 24 23 co 
 |-  ( ( g ` x ) ( +g ` t ) ( g ` y ) )
26 21 25 wceq 
 |-  ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
27 26 15 10 wral 
 |-  A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
28 27 14 10 wral 
 |-  A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
29 13 28 wa 
 |-  ( g : w --> ( Base ` t ) /\ A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) ) )
30 29 8 7 wsbc 
 |-  [. ( 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 ) ) )
31 30 4 cab 
 |-  { 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 ) ) ) }
32 1 3 2 2 31 cmpo 
 |-  ( 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 ) ) ) } )
33 0 32 wceq 
 |-  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 ) ) ) } )