Theorem unitrinv

Description: A unit times its inverse is the ring unity. (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	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	unitinvcl.4	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	unitrinv	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{·}I\left(X\right)=\underset{\dot{}}{1}$$

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	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		unitinvcl.4	$$⊢\underset{\dot{}}{1}=1_R$$
5		eqid	$$⊢{\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U$$
6	1 5	unitgrp	$$⊢R\in \mathrm{Ring}\to {\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}$$
7	1 5	unitgrpbas	$$⊢U={\mathrm{Base}}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
8	1	fvexi	$$⊢U\in \mathrm{V}$$
9		eqid	$$⊢{\mathrm{mulGrp}}_R={\mathrm{mulGrp}}_R$$
10	9 3	mgpplusg	$$⊢\underset{\dot{}}{·}={+}_{{\mathrm{mulGrp}}_R}$$
11	5 10	ressplusg	$$⊢U\in \mathrm{V}\to \underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
12	8 11	ax-mp	$$⊢\underset{\dot{}}{·}={+}_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
13		eqid	$$⊢0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
14	1 5 2	invrfval	$$⊢I={inv}_g\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)$$
15	7 12 13 14	grprinv	$$⊢\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\in \mathrm{Grp}\wedge X\in U\right)\to X\underset{\dot{}}{·}I\left(X\right)=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
16	6 15	sylan	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{·}I\left(X\right)=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
17	1 5 4	unitgrpid	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
18	17	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to \underset{\dot{}}{1}=0_{\left({\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}U\right)}$$
19	16 18	eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge X\in U\right)\to X\underset{\dot{}}{·}I\left(X\right)=\underset{\dot{}}{1}$$