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=\mathrm{Unit}\left(R\right)$$
	unitinvcl.2	$$⊢I={inv}_r\left(R\right)$$
	ringinvcl.3	$$⊢B={\mathrm{Base}}_R$$
Assertion	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitinvcl.2	$$⊢I={inv}_r\left(R\right)$$
3		ringinvcl.3	$$⊢B={\mathrm{Base}}_R$$
4	1 2	unitinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)\in U$$
5	3 1	unitcl	$$⊢I\left(X\right)\in U\to I\left(X\right)\in B$$
6	4 5	syl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)\in B$$