Theorem 0ring

Description: If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		0ring.b	$$⊢B={\mathrm{Base}}_R$$
2		0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
3	1 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
4	1	fvexi	$$⊢B\in \mathrm{V}$$
5		hashen1	$$⊢B\in \mathrm{V}\to \left(\left|B\right|=1\leftrightarrow B\approx 1_{𝑜}\right)$$
6	4 5	ax-mp	$$⊢\left|B\right|=1\leftrightarrow B\approx 1_{𝑜}$$
7		en1eqsn	$$⊢\left(\underset{\dot{}}{0}\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
8	7	ex	$$⊢\underset{\dot{}}{0}\in B\to \left(B\approx 1_{𝑜}\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
9	6 8	syl5bi	$$⊢\underset{\dot{}}{0}\in B\to \left(\left|B\right|=1\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
10	3 9	syl	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
11	10	imp	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$