Theorem 0ringbas

Description: The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		0ringdif.b	$$⊢B={\mathrm{Base}}_R$$
2		0ringdif.0	$$⊢\underset{\dot{}}{0}=0_R$$
3	1 2	0ringdif	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge B=\left\{\underset{\dot{}}{0}\right\}\right)$$
4	3	simprbi	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$