Definition df-ghm 16139

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 16138	. 2 class GrpHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cgrp 15927	. . 3 class Grp
5		vw	. . . . . . . 8 setvar w
6	5	cv 1382	. . . . . . 7 class w
7	3	cv 1382	. . . . . . . 8 class t
8		cbs 14509	. . . . . . . 8 class Base
9	7, 8	cfv 5578	. . . . . . 7 class ( Base ` t )
10		vg	. . . . . . . 8 setvar g
11	10	cv 1382	. . . . . . 7 class g
12	6, 9, 11	wf 5574	. . . . . 6 wff g : w --> ( Base ` t )
13		vx	. . . . . . . . . . . 12 setvar x
14	13	cv 1382	. . . . . . . . . . 11 class x
15		vy	. . . . . . . . . . . 12 setvar y
16	15	cv 1382	. . . . . . . . . . 11 class y
17	2	cv 1382	. . . . . . . . . . . 12 class s
18		cplusg 14574	. . . . . . . . . . . 12 class +g
19	17, 18	cfv 5578	. . . . . . . . . . 11 class ( +g ` s )
20	14, 16, 19	co 6281	. . . . . . . . . 10 class ( x ( +g ` s ) y )
21	20, 11	cfv 5578	. . . . . . . . 9 class ( g ` ( x ( +g ` s ) y ) )
22	14, 11	cfv 5578	. . . . . . . . . 10 class ( g ` x )
23	16, 11	cfv 5578	. . . . . . . . . 10 class ( g ` y )
24	7, 18	cfv 5578	. . . . . . . . . 10 class ( +g ` t )
25	22, 23, 24	co 6281	. . . . . . . . 9 class ( ( g ` x ) ( +g ` t ) ( g ` y ) )
26	21, 25	wceq 1383	. . . . . . . 8 wff ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
27	26, 15, 6	wral 2793	. . . . . . 7 wff A. y e. w ( g ` ( x ( +g ` s ) y ) ) = ( ( g ` x ) ( +g ` t ) ( g ` y ) )
28	27, 13, 6	wral 2793	. . . . . 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 369	. . . . 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 5578	. . . . 5 class ( Base ` s )
31	29, 5, 30	wsbc 3313	. . . 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 2428	. . 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 6283	. 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 1383	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  16140  isghm  16141