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 = ( Unit ` R )
	unitinvcl.2	|- I = ( invr ` R )
Assertion	unitinvinv	|- ( ( R e. Ring /\ X e. U ) -> ( I ` ( I ` X ) ) = X )

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	|- U = ( Unit ` R )
2		unitinvcl.2	|- I = ( invr ` R )
3		eqid	|- ( ( mulGrp ` R ) |`s U ) = ( ( mulGrp ` R ) |`s U )
4	1 3	unitgrp	|- ( R e. Ring -> ( ( mulGrp ` R ) |`s U ) e. Grp )
5	1 3	unitgrpbas	|- U = ( Base ` ( ( mulGrp ` R ) |`s U ) )
6	1 3 2	invrfval	|- I = ( invg ` ( ( mulGrp ` R ) |`s U ) )
7	5 6	grpinvinv	|- ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ X e. U ) -> ( I ` ( I ` X ) ) = X )
8	4 7	sylan	|- ( ( R e. Ring /\ X e. U ) -> ( I ` ( I ` X ) ) = X )