Theorem drnginvrl

Description: Property of the multiplicative inverse in a division ring. ( recid2 analog.) (Contributed by NM, 19-Apr-2014)

	Ref	Expression
Hypotheses	drnginvrl.b	$$⊢B={\mathrm{Base}}_R$$
	drnginvrl.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drnginvrl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	drnginvrl.u	$$⊢\underset{\dot{}}{1}=1_R$$
	drnginvrl.i	$$⊢I={inv}_r\left(R\right)$$
Assertion	drnginvrl	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		drnginvrl.b	$$⊢B={\mathrm{Base}}_R$$
2		drnginvrl.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		drnginvrl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
4		drnginvrl.u	$$⊢\underset{\dot{}}{1}=1_R$$
5		drnginvrl.i	$$⊢I={inv}_r\left(R\right)$$
6		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
7	1 6 2	drngunit	$$⊢R\in \mathrm{DivRing}\to \left(X\in \mathrm{Unit}\left(R\right)\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\right)$$
8		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
9	6 5 3 4	unitlinv	$$⊢\left(R\in \mathrm{Ring}\wedge X\in \mathrm{Unit}\left(R\right)\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$
10	9	ex	$$⊢R\in \mathrm{Ring}\to \left(X\in \mathrm{Unit}\left(R\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
11	8 10	syl	$$⊢R\in \mathrm{DivRing}\to \left(X\in \mathrm{Unit}\left(R\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
12	7 11	sylbird	$$⊢R\in \mathrm{DivRing}\to \left(\left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}\right)$$
13	12	3impib	$$⊢\left(R\in \mathrm{DivRing}\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to I\left(X\right)\underset{\dot{}}{·}X=\underset{\dot{}}{1}$$