Description: The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | idghm.b | |
|
Assertion | idghm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idghm.b | |
|
2 | id | |
|
3 | eqid | |
|
4 | 1 3 | grpcl | |
5 | 4 | 3expb | |
6 | fvresi | |
|
7 | 5 6 | syl | |
8 | fvresi | |
|
9 | fvresi | |
|
10 | 8 9 | oveqan12d | |
11 | 10 | adantl | |
12 | 7 11 | eqtr4d | |
13 | 12 | ralrimivva | |
14 | f1oi | |
|
15 | f1of | |
|
16 | 14 15 | ax-mp | |
17 | 13 16 | jctil | |
18 | 1 1 3 3 | isghm | |
19 | 2 2 17 18 | syl21anbrc | |