Theorem isdrng

Description: The predicate "is a division ring". (Contributed by NM, 18-Oct-2012) (Revised 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	isdrng	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge U=B\setminus \left\{\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		fveq2	$$⊢r=R\to \mathrm{Unit}\left(r\right)=\mathrm{Unit}\left(R\right)$$
5	4 2	eqtr4di	$$⊢r=R\to \mathrm{Unit}\left(r\right)=U$$
6		fveq2	$$⊢r=R\to {\mathrm{Base}}_r={\mathrm{Base}}_R$$
7	6 1	eqtr4di	$$⊢r=R\to {\mathrm{Base}}_r=B$$
8		fveq2	$$⊢r=R\to 0_r=0_R$$
9	8 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
10	9	sneqd	$$⊢r=R\to \left\{0_r\right\}=\left\{\underset{\dot{}}{0}\right\}$$
11	7 10	difeq12d	$$⊢r=R\to {\mathrm{Base}}_r\setminus \left\{0_r\right\}=B\setminus \left\{\underset{\dot{}}{0}\right\}$$
12	5 11	eqeq12d	$$⊢r=R\to \left(\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}\leftrightarrow U=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13		df-drng	$$⊢\mathrm{DivRing}=\left\{r\in \mathrm{Ring}|\mathrm{Unit}\left(r\right)={\mathrm{Base}}_r\setminus \left\{0_r\right\}\right\}$$
14	12 13	elrab2	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge U=B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$