This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = Unit ⁡ R
unitinvcl.2 ⊢ I = inv r ⁡ R
Assertion unitinvcl ⊢ R ∈ Ring ∧ X ∈ U → I ⁡ X ∈ U

Proof

Step Hyp Ref Expression
1 unitinvcl.1 ⊢ U = Unit ⁡ R
2 unitinvcl.2 ⊢ I = inv r ⁡ R
3 eqid ⊢ mulGrp R ↾ 𝑠 U = mulGrp R ↾ 𝑠 U
4 1 3 unitgrp ⊢ R ∈ Ring → mulGrp R ↾ 𝑠 U ∈ Grp
5 1 3 unitgrpbas ⊢ U = Base mulGrp R ↾ 𝑠 U
6 1 3 2 invrfval ⊢ I = inv g ⁡ mulGrp R ↾ 𝑠 U
7 5 6 grpinvcl ⊢ mulGrp R ↾ 𝑠 U ∈ Grp ∧ X ∈ U → I ⁡ X ∈ U
8 4 7 sylan ⊢ R ∈ Ring ∧ X ∈ U → I ⁡ X ∈ U