Theorem 0ring01eqbi

Description: In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by AV, 23-Jan-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	0ring01eqbi	$$⊢R\in \mathrm{Ring}\to \left(B\approx 1_{𝑜}\leftrightarrow \underset{\dot{}}{1}=\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		0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
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	mp1i	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\leftrightarrow B\approx 1_{𝑜}\right)$$
7	1 2 3	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
8	7	eqcomd	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
9	8	ex	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
10		eqcom	$$⊢\underset{\dot{}}{1}=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
11	1 2 3	01eq0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
12		fveq2	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=\left|\left\{\underset{\dot{}}{0}\right\}\right|$$
13	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
14		hashsng	$$⊢\underset{\dot{}}{0}\in \mathrm{V}\to \left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
15	13 14	mp1i	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
16	12 15	eqtrd	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=1$$
17	11 16	syl	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \left|B\right|=1$$
18	17	ex	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}=\underset{\dot{}}{1}\to \left|B\right|=1\right)$$
19	10 18	syl5bi	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{1}=\underset{\dot{}}{0}\to \left|B\right|=1\right)$$
20	9 19	impbid	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|=1\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
21	6 20	bitr3d	$$⊢R\in \mathrm{Ring}\to \left(B\approx 1_{𝑜}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$