Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ghm Structured version   Unicode version

Definition df-ghm 15009
 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
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-ghm
StepHypRef Expression
1 cghm 15008 . 2
2 vs . . 3
3 vt . . 3
4 cgrp 14690 . . 3
5 vw . . . . . . . 8
65cv 1652 . . . . . . 7
73cv 1652 . . . . . . . 8
8 cbs 13474 . . . . . . . 8
97, 8cfv 5457 . . . . . . 7
10 vg . . . . . . . 8
1110cv 1652 . . . . . . 7
126, 9, 11wf 5453 . . . . . 6
13 vx . . . . . . . . . . . 12
1413cv 1652 . . . . . . . . . . 11
15 vy . . . . . . . . . . . 12
1615cv 1652 . . . . . . . . . . 11
172cv 1652 . . . . . . . . . . . 12
18 cplusg 13534 . . . . . . . . . . . 12
1917, 18cfv 5457 . . . . . . . . . . 11
2014, 16, 19co 6084 . . . . . . . . . 10
2120, 11cfv 5457 . . . . . . . . 9
2214, 11cfv 5457 . . . . . . . . . 10
2316, 11cfv 5457 . . . . . . . . . 10
247, 18cfv 5457 . . . . . . . . . 10
2522, 23, 24co 6084 . . . . . . . . 9
2621, 25wceq 1653 . . . . . . . 8
2726, 15, 6wral 2707 . . . . . . 7
2827, 13, 6wral 2707 . . . . . 6
2912, 28wa 360 . . . . 5
3017, 8cfv 5457 . . . . 5
3129, 5, 30wsbc 3163 . . . 4
3231, 10cab 2424 . . 3
332, 3, 4, 4, 32cmpt2 6086 . 2
341, 33wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  reldmghm  15010  isghm  15011
 Copyright terms: Public domain W3C validator