Definition df-ghm 18747

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 = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))})

Distinct variable group:   𝑔,𝑠,𝑡,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-ghm

Step	Hyp	Ref	Expression
1		cghm 18746	. 2 class GrpHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cgrp 18492	. . 3 class Grp
5		vw	. . . . . . . 8 setvar 𝑤
6	5	cv 1538	. . . . . . 7 class 𝑤
7	3	cv 1538	. . . . . . . 8 class 𝑡
8		cbs 16840	. . . . . . . 8 class Base
9	7, 8	cfv 6418	. . . . . . 7 class (Base‘𝑡)
10		vg	. . . . . . . 8 setvar 𝑔
11	10	cv 1538	. . . . . . 7 class 𝑔
12	6, 9, 11	wf 6414	. . . . . 6 wff 𝑔:𝑤⟶(Base‘𝑡)
13		vx	. . . . . . . . . . . 12 setvar 𝑥
14	13	cv 1538	. . . . . . . . . . 11 class 𝑥
15		vy	. . . . . . . . . . . 12 setvar 𝑦
16	15	cv 1538	. . . . . . . . . . 11 class 𝑦
17	2	cv 1538	. . . . . . . . . . . 12 class 𝑠
18		cplusg 16888	. . . . . . . . . . . 12 class +g
19	17, 18	cfv 6418	. . . . . . . . . . 11 class (+g‘𝑠)
20	14, 16, 19	co 7255	. . . . . . . . . 10 class (𝑥(+g‘𝑠)𝑦)
21	20, 11	cfv 6418	. . . . . . . . 9 class (𝑔‘(𝑥(+g‘𝑠)𝑦))
22	14, 11	cfv 6418	. . . . . . . . . 10 class (𝑔‘𝑥)
23	16, 11	cfv 6418	. . . . . . . . . 10 class (𝑔‘𝑦)
24	7, 18	cfv 6418	. . . . . . . . . 10 class (+g‘𝑡)
25	22, 23, 24	co 7255	. . . . . . . . 9 class ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))
26	21, 25	wceq 1539	. . . . . . . 8 wff (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))
27	26, 15, 6	wral 3063	. . . . . . 7 wff ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))
28	27, 13, 6	wral 3063	. . . . . 6 wff ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦))
29	12, 28	wa 395	. . . . 5 wff (𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))
30	17, 8	cfv 6418	. . . . 5 class (Base‘𝑠)
31	29, 5, 30	wsbc 3711	. . . 4 wff [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))
32	31, 10	cab 2715	. . 3 class {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))}
33	2, 3, 4, 4, 32	cmpo 7257	. 2 class (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))})
34	1, 33	wceq 1539	1 wff GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))})

This definition is referenced by:  reldmghm  18748  isghm  18749