Theorem drngui

Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	drngui.b	$$⊢B={\mathrm{Base}}_R$$
	drngui.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drngui.r	$$⊢R\in \mathrm{DivRing}$$
Assertion	drngui	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		drngui.b	$$⊢B={\mathrm{Base}}_R$$
2		drngui.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngui.r	$$⊢R\in \mathrm{DivRing}$$
4		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
5	1 4 2	isdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge \mathrm{Unit}\left(R\right)=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
6	3 5	mpbi	$$⊢\left(R\in \mathrm{Ring}\wedge \mathrm{Unit}\left(R\right)=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
7	6	simpri	$$⊢\mathrm{Unit}\left(R\right)=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
8	7	eqcomi	$$⊢B\setminus \left\{\underset{\dot{}}{0}\right\}=\mathrm{Unit}\left(R\right)$$