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

Proof

Step	Hyp	Ref	Expression
1		unitinvcl.1	$$⊢U=\mathrm{Unit}\left(R\right)$$
2		unitinvcl.2	$$⊢I={inv}_r\left(R\right)$$
3		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
4	1 3	unitgrp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
5	1 3	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
6	1 3 2	invrfval	$$⊢I={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)$$
7	5 6	grpinvcl	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge X\in U\right)\to I\left(X\right)\in U$$
8	4 7	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to I\left(X\right)\in U$$