# Metamath Proof Explorer

## Theorem unitlinv

Description: A unit times its inverse is the identity. (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)$
unitinvcl.3
unitinvcl.4
Assertion unitlinv

### Proof

Step Hyp Ref Expression
1 unitinvcl.1 ${⊢}{U}=\mathrm{Unit}\left({R}\right)$
2 unitinvcl.2 ${⊢}{I}={inv}_{r}\left({R}\right)$
3 unitinvcl.3
4 unitinvcl.4
5 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}={\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}$
6 1 5 unitgrp ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\in \mathrm{Grp}$
7 1 5 unitgrpbas ${⊢}{U}={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)}$
8 1 fvexi ${⊢}{U}\in \mathrm{V}$
9 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
10 9 3 mgpplusg
11 5 10 ressplusg
12 8 11 ax-mp
13 eqid ${⊢}{0}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)}={0}_{\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)}$
14 1 5 2 invrfval ${⊢}{I}={inv}_{g}\left({\mathrm{mulGrp}}_{{R}}{↾}_{𝑠}{U}\right)$
15 7 12 13 14 grplinv
16 6 15 sylan
17 1 5 4 unitgrpid
18 17 adantr
19 16 18 eqtr4d