Theorem 0ringdif

Description: A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		0ringdif.b	$$⊢B={\mathrm{Base}}_R$$
2		0ringdif.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		eldif	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge \neg R\in \mathrm{NzRing}\right)$$
4	1	a1i	$$⊢R\in \mathrm{Ring}\to B={\mathrm{Base}}_R$$
5	4	fveqeq2d	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\leftrightarrow \left|{\mathrm{Base}}_R\right|=1\right)$$
6	1 2	0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
7	6	ex	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
8		fveq2	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=\left|\left\{\underset{\dot{}}{0}\right\}\right|$$
9	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10		hashsng	$$⊢\underset{\dot{}}{0}\in \mathrm{V}\to \left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
11	9 10	ax-mp	$$⊢\left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
12	8 11	eqtrdi	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=1$$
13	7 12	impbid1	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\leftrightarrow B=\left\{\underset{\dot{}}{0}\right\}\right)$$
14		0ringnnzr	$$⊢R\in \mathrm{Ring}\to \left(\left|{\mathrm{Base}}_R\right|=1\leftrightarrow \neg R\in \mathrm{NzRing}\right)$$
15	5 13 14	3bitr3rd	$$⊢R\in \mathrm{Ring}\to \left(\neg R\in \mathrm{NzRing}\leftrightarrow B=\left\{\underset{\dot{}}{0}\right\}\right)$$
16	15	pm5.32i	$$⊢\left(R\in \mathrm{Ring}\wedge \neg R\in \mathrm{NzRing}\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge B=\left\{\underset{\dot{}}{0}\right\}\right)$$
17	3 16	bitri	$$⊢R\in \left(\mathrm{Ring}\setminus \mathrm{NzRing}\right)\leftrightarrow \left(R\in \mathrm{Ring}\wedge B=\left\{\underset{\dot{}}{0}\right\}\right)$$