Theorem 1rinv

Description: The inverse of the ring unity is the ring unity. (Contributed by Mario Carneiro, 18-Jun-2015)

	Ref	Expression
Hypotheses	1rinv.1	$$⊢I={inv}_r\left(R\right)$$
	1rinv.2	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	1rinv	$$⊢R\in \mathrm{Ring}\to I\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		1rinv.1	$$⊢I={inv}_r\left(R\right)$$
2		1rinv.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
4	3 2	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	3 1 5	ringinvcl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)\right)\to I\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R$$
7	4 6	mpdan	$$⊢R\in \mathrm{Ring}\to I\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R$$
8		eqid	$$⊢{\cdot }_R={\cdot }_R$$
9	5 8 2	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge I\left(\underset{\dot{}}{1}\right)\in {\mathrm{Base}}_R\right)\to \underset{\dot{}}{1}{\cdot }_{R}I\left(\underset{\dot{}}{1}\right)=I\left(\underset{\dot{}}{1}\right)$$
10	7 9	mpdan	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}{\cdot }_{R}I\left(\underset{\dot{}}{1}\right)=I\left(\underset{\dot{}}{1}\right)$$
11	3 1 8 2	unitrinv	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)\right)\to \underset{\dot{}}{1}{\cdot }_{R}I\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
12	4 11	mpdan	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}{\cdot }_{R}I\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$
13	10 12	eqtr3d	$$⊢R\in \mathrm{Ring}\to I\left(\underset{\dot{}}{1}\right)=\underset{\dot{}}{1}$$