Description: If the difference between two group elements is zero, they are equal. ( subeq0 analog.) (Contributed by NM, 31-Mar-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpsubid.b | |
|
grpsubid.o | |
||
grpsubid.m | |
||
Assertion | grpsubeq0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpsubid.b | |
|
2 | grpsubid.o | |
|
3 | grpsubid.m | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 4 5 3 | grpsubval | |
7 | 6 | 3adant1 | |
8 | 7 | eqeq1d | |
9 | simp1 | |
|
10 | 1 5 | grpinvcl | |
11 | 10 | 3adant2 | |
12 | simp2 | |
|
13 | 1 4 2 5 | grpinvid2 | |
14 | 9 11 12 13 | syl3anc | |
15 | 1 5 | grpinvinv | |
16 | 15 | 3adant2 | |
17 | 16 | eqeq1d | |
18 | eqcom | |
|
19 | 17 18 | bitrdi | |
20 | 8 14 19 | 3bitr2d | |