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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cghm | |
|
1 | vs | |
|
2 | cgrp | |
|
3 | vt | |
|
4 | vg | |
|
5 | cbs | |
|
6 | 1 | cv | |
7 | 6 5 | cfv | |
8 | vw | |
|
9 | 4 | cv | |
10 | 8 | cv | |
11 | 3 | cv | |
12 | 11 5 | cfv | |
13 | 10 12 9 | wf | |
14 | vx | |
|
15 | vy | |
|
16 | 14 | cv | |
17 | cplusg | |
|
18 | 6 17 | cfv | |
19 | 15 | cv | |
20 | 16 19 18 | co | |
21 | 20 9 | cfv | |
22 | 16 9 | cfv | |
23 | 11 17 | cfv | |
24 | 19 9 | cfv | |
25 | 22 24 23 | co | |
26 | 21 25 | wceq | |
27 | 26 15 10 | wral | |
28 | 27 14 10 | wral | |
29 | 13 28 | wa | |
30 | 29 8 7 | wsbc | |
31 | 30 4 | cab | |
32 | 1 3 2 2 31 | cmpo | |
33 | 0 32 | wceq | |