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=sGrp,tGrpg|[˙Bases/w]˙g:wBasetxwywgx+sy=gx+tgy

Detailed syntax breakdown

Step Hyp Ref Expression
0 cghm classGrpHom
1 vs setvars
2 cgrp classGrp
3 vt setvart
4 vg setvarg
5 cbs classBase
6 1 cv setvars
7 6 5 cfv classBases
8 vw setvarw
9 4 cv setvarg
10 8 cv setvarw
11 3 cv setvart
12 11 5 cfv classBaset
13 10 12 9 wf wffg:wBaset
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 classx+sy
21 20 9 cfv classgx+sy
22 16 9 cfv classgx
23 11 17 cfv class+t
24 19 9 cfv classgy
25 22 24 23 co classgx+tgy
26 21 25 wceq wffgx+sy=gx+tgy
27 26 15 10 wral wffywgx+sy=gx+tgy
28 27 14 10 wral wffxwywgx+sy=gx+tgy
29 13 28 wa wffg:wBasetxwywgx+sy=gx+tgy
30 29 8 7 wsbc wff[˙Bases/w]˙g:wBasetxwywgx+sy=gx+tgy
31 30 4 cab classg|[˙Bases/w]˙g:wBasetxwywgx+sy=gx+tgy
32 1 3 2 2 31 cmpo classsGrp,tGrpg|[˙Bases/w]˙g:wBasetxwywgx+sy=gx+tgy
33 0 32 wceq wffGrpHom=sGrp,tGrpg|[˙Bases/w]˙g:wBasetxwywgx+sy=gx+tgy