Description: Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpoinveu.1 | |
|
grpoinveu.2 | |
||
Assertion | grpoid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpoinveu.1 | |
|
2 | grpoinveu.2 | |
|
3 | 1 2 | grpoidcl | |
4 | 1 | grporcan | |
5 | 4 | 3exp2 | |
6 | 3 5 | mpid | |
7 | 6 | pm2.43d | |
8 | 7 | imp | |
9 | 1 2 | grpolid | |
10 | 9 | eqeq2d | |
11 | 8 10 | bitr3d | |