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	$$⊢\mathrm{GrpHom}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cghm	$$class\mathrm{GrpHom}$$
1		vs	$$setvars$$
2		cgrp	$$class\mathrm{Grp}$$
3		vt	$$setvart$$
4		vg	$$setvarg$$
5		cbs	$$class\mathrm{Base}$$
6	1	cv	$$setvars$$
7	6 5	cfv	$$class{\mathrm{Base}}_s$$
8		vw	$$setvarw$$
9	4	cv	$$setvarg$$
10	8	cv	$$setvarw$$
11	3	cv	$$setvart$$
12	11 5	cfv	$$class{\mathrm{Base}}_t$$
13	10 12 9	wf	$$wffg:w⟶{\mathrm{Base}}_t$$
14		vx	$$setvarx$$
15		vy	$$setvary$$
16	14	cv	$$setvarx$$
17		cplusg	$$class{+}_{𝑔}$$
18	6 17	cfv	$$class{+}_s$$
19	15	cv	$$setvary$$
20	16 19 18	co	$$class\left(x{+}_{s}y\right)$$
21	20 9	cfv	$$classg\left(x{+}_{s}y\right)$$
22	16 9	cfv	$$classg\left(x\right)$$
23	11 17	cfv	$$class{+}_t$$
24	19 9	cfv	$$classg\left(y\right)$$
25	22 24 23	co	$$class\left(g\left(x\right){+}_{t}g\left(y\right)\right)$$
26	21 25	wceq	$$wffg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)$$
27	26 15 10	wral	$$wff\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)$$
28	27 14 10	wral	$$wff\forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)$$
29	13 28	wa	$$wff\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)$$
30	29 8 7	wsbc	$$wff\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)$$
31	30 4	cab	$$class\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)\right\}$$
32	1 3 2 2 31	cmpo	$$class\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)\right\}\right)$$
33	0 32	wceq	$$wff\mathrm{GrpHom}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)\right\}\right)$$