Theorem 0ring1eq0

Description: In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	0ring.b	$$⊢B={\mathrm{Base}}_R$$
	0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
	0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	0ring1eq0	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		0ring.b	$$⊢B={\mathrm{Base}}_R$$
2		0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		eldif	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge \neg R\in \mathrm{NzRing}\right)$$
5		0ringnnzr	$$⊢R\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_R\right|=1\leftrightarrow \neg R\in \mathrm{NzRing}\right)$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7	6 2 3	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|{\mathrm{Base}}_R\right|=1\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
8	7	eqcomd	$$⊢\left(R\in \mathrm{Ring}\wedge \left|{\mathrm{Base}}_R\right|=1\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
9	8	ex	$$⊢R\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_R\right|=1\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
10	5 9	sylbird	$$⊢R\in \mathrm{Ring}\to \left(\neg R\in \mathrm{NzRing}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
11	10	imp	$$⊢\left(R\in \mathrm{Ring}\wedge \neg R\in \mathrm{NzRing}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
12	4 11	sylbi	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$