Theorem drngunz

Description: A division ring's unity is different from its zero. (Contributed by NM, 8-Sep-2011)

	Ref	Expression
Hypotheses	drngunz.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drngunz.u	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	drngunz	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		drngunz.z	$$⊢\underset{\dot{}}{0}=0_R$$
2		drngunz.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
4		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
5	4 2	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
6	3 5	syl	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
7		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
8	7 4 1	drngunit	$$⊢R\in \mathrm{DivRing}\to \left(\underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)\leftrightarrow \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)\right)$$
9	6 8	mpbid	$$⊢R\in \mathrm{DivRing}\to \left(\underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge \underset{\dot{}}{1}\ne \underset{\dot{}}{0}\right)$$
10	9	simprd	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$