Theorem ringinvcl

Description: The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	|- U = ( Unit ` R )
2		unitinvcl.2	|- I = ( invr ` R )
3		ringinvcl.3	|- B = ( Base ` R )
4	1 2	unitinvcl	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )
5	3 1	unitcl	|- ( ( I ` X ) e. U -> ( I ` X ) e. B )
6	4 5	syl	|- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B )