Metamath Proof Explorer


Theorem unitinvinv

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 U=UnitR
unitinvcl.2 I=invrR
Assertion unitinvinv RRingXUIIX=X

Proof

Step Hyp Ref Expression
1 unitinvcl.1 U=UnitR
2 unitinvcl.2 I=invrR
3 eqid mulGrpR𝑠U=mulGrpR𝑠U
4 1 3 unitgrp RRingmulGrpR𝑠UGrp
5 1 3 unitgrpbas U=BasemulGrpR𝑠U
6 1 3 2 invrfval I=invgmulGrpR𝑠U
7 5 6 grpinvinv mulGrpR𝑠UGrpXUIIX=X
8 4 7 sylan RRingXUIIX=X