Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019)

	Ref	Expression
Hypotheses	0ring.b	$$⊢B={\mathrm{Base}}_R$$
	0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
	0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	01eq0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{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		0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
4	1	fvexi	$$⊢B\in \mathrm{V}$$
5		hashv01gt1	$$⊢B\in \mathrm{V}\to \left(\left|B\right|=0\vee \left|B\right|=1\vee 1<\left|B\right|\right)$$
6	4 5	ax-mp	$$⊢\left(\left|B\right|=0\vee \left|B\right|=1\vee 1<\left|B\right|\right)$$
7		hasheq0	$$⊢B\in \mathrm{V}\to \left(\left|B\right|=0\leftrightarrow B=\varnothing \right)$$
8	4 7	ax-mp	$$⊢\left|B\right|=0\leftrightarrow B=\varnothing$$
9		ne0i	$$⊢\underset{\dot{}}{0}\in B\to B\ne \varnothing$$
10		eqneqall	$$⊢B=\varnothing \to \left(B\ne \varnothing \to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
11	9 10	syl5com	$$⊢\underset{\dot{}}{0}\in B\to \left(B=\varnothing \to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
12	8 11	syl5bi	$$⊢\underset{\dot{}}{0}\in B\to \left(\left|B\right|=0\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
13	1 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
14	12 13	syl11	$$⊢\left|B\right|=0\to \left(R\in \mathrm{Ring}\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
15		eqneqall	$$⊢\left|B\right|=1\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)$$
16	15	a1d	$$⊢\left|B\right|=1\to \left(R\in \mathrm{Ring}\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
17	1 3 2	ring1ne0	$$⊢\left(R\in \mathrm{Ring}\wedge 1<\left|B\right|\right)\to \underset{\dot{}}{1}\ne \underset{\dot{}}{0}$$
18	17	necomd	$$⊢\left(R\in \mathrm{Ring}\wedge 1<\left|B\right|\right)\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}$$
19	18	ex	$$⊢R\in \mathrm{Ring}\to \left(1<\left|B\right|\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)$$
20	19	a1i	$$⊢\left|B\right|\ne 1\to \left(R\in \mathrm{Ring}\to \left(1<\left|B\right|\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
21	20	com13	$$⊢1<\left|B\right|\to \left(R\in \mathrm{Ring}\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
22	14 16 21	3jaoi	$$⊢\left(\left|B\right|=0\vee \left|B\right|=1\vee 1<\left|B\right|\right)\to \left(R\in \mathrm{Ring}\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)\right)$$
23	6 22	ax-mp	$$⊢R\in \mathrm{Ring}\to \left(\left|B\right|\ne 1\to \underset{\dot{}}{0}\ne \underset{\dot{}}{1}\right)$$
24	23	necon4d	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}=\underset{\dot{}}{1}\to \left|B\right|=1\right)$$
25	24	imp	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to \left|B\right|=1$$
26	1 2	0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
27	25 26	syldan	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$