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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 unitinvcl.1 ⊢ U = Unit ⁡ R
2 unitinvcl.2 ⊢ I = inv r ⁡ R
3 ringinvcl.3 ⊢ B = Base R
4 1 2 unitinvcl ⊢ R ∈ Ring ∧ X ∈ U → I ⁡ X ∈ U
5 3 1 unitcl ⊢ I ⁡ X ∈ U → I ⁡ X ∈ B
6 4 5 syl ⊢ R ∈ Ring ∧ X ∈ U → I ⁡ X ∈ B