Definition df-ghm 14959

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

Step	Hyp	Ref	Expression
1		cghm 14958	. 2 class GrpHom
2		vs	. . 3 set s
3		vt	. . 3 set t
4		cgrp 14640	. . 3 class Grp
5		vw	. . . . . . . 8 set w
6	5	cv 1648	. . . . . . 7 class w
7	3	cv 1648	. . . . . . . 8 class t
8		cbs 13424	. . . . . . . 8 class Base
9	7, 8	cfv 5413	. . . . . . 7 class ( Base ` t )
10		vg	. . . . . . . 8 set g
11	10	cv 1648	. . . . . . 7 class g
12	6, 9, 11	wf 5409	. . . . . 6 wff g : w --> ( Base ` t )
13		vx	. . . . . . . . . . . 12 set x
14	13	cv 1648	. . . . . . . . . . 11 class x
15		vy	. . . . . . . . . . . 12 set y
16	15	cv 1648	. . . . . . . . . . 11 class y
17	2	cv 1648	. . . . . . . . . . . 12 class s
18		cplusg 13484	. . . . . . . . . . . 12 class +g
19	17, 18	cfv 5413	. . . . . . . . . . 11 class ( +g ` s )
20	14, 16, 19	co 6040	. . . . . . . . . 10 class ( x ( +g ` s ) y )
21	20, 11	cfv 5413	. . . . . . . . 9 class ( g ` ( x ( +g ` s ) y ) )
22	14, 11	cfv 5413	. . . . . . . . . 10 class ( g ` x )
23	16, 11	cfv 5413	. . . . . . . . . 10 class ( g ` y )
24	7, 18	cfv 5413	. . . . . . . . . 10 class ( +g ` t )
25	22, 23, 24	co 6040	. . . . . . . . 9 class ( ( g ` x ) ( +g ` t ) ( g ` y ) )
26	21, 25	wceq 1649	. . . . . . . 8 wff ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
27	26, 15, 6	wral 2666	. . . . . . 7 wff A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
28	27, 13, 6	wral 2666	. . . . . 6 wff A. x e. w A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
29	12, 28	wa 359	. . . . 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 ) ) )
30	17, 8	cfv 5413	. . . . 5 class ( Base ` s )
31	29, 5, 30	wsbc 3121	. . . 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 ) ) )
32	31, 10	cab 2390	. . 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 ) ) ) }
33	2, 3, 4, 4, 32	cmpt2 6042	. 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 ) ) ) } )
34	1, 33	wceq 1649	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 ) ) ) } )

This definition is referenced by:  reldmghm  14960  isghm  14961