Theorem unitinvcl

Description: The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	unitinvcl.1	|- U = ( Unit ` R )
	unitinvcl.2	|- I = ( invr ` R )
Assertion	unitinvcl	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )

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	grpinvcl	|- ( ( ( ( mulGrp ` R ) |`s U ) e. Grp /\ X e. U ) -> ( I ` X ) e. U )
8	4 7	sylan	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )