Theorem drngunit

Description: Elementhood in the set of units when R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	isdrng.b	$$⊢B={\mathrm{Base}}_R$$
	isdrng.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
	isdrng.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	drngunit	$$⊢R\in \mathrm{DivRing}\to \left(X\in U\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdrng.b	$$⊢B={\mathrm{Base}}_R$$
2		isdrng.u	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		isdrng.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 2 3	isdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge U=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
5	4	simprbi	$$⊢R\in \mathrm{DivRing}\to U=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
6	5	eleq2d	$$⊢R\in \mathrm{DivRing}\to \left(X\in U\leftrightarrow X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
7		eldifsn	$$⊢X\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)$$
8	6 7	bitrdi	$$⊢R\in \mathrm{DivRing}\to \left(X\in U\leftrightarrow \left(X\in B\wedge X\ne \underset{\dot{}}{0}\right)\right)$$