Description: The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | unitinvcl.1 | |
|
unitinvcl.2 | |
||
Assertion | unitinvinv | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unitinvcl.1 | |
|
2 | unitinvcl.2 | |
|
3 | eqid | |
|
4 | 1 3 | unitgrp | |
5 | 1 3 | unitgrpbas | |
6 | 1 3 2 | invrfval | |
7 | 5 6 | grpinvinv | |
8 | 4 7 | sylan | |