# Metamath Proof Explorer

## 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}}{↾}_{𝑠}{U}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
4 1 3 unitgrp ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\in \mathrm{Grp}$
5 1 3 unitgrpbas ${⊢}{U}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)}$
6 1 3 2 invrfval ${⊢}{I}={inv}_{g}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)$
7 5 6 grpinvcl ${⊢}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{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}$