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) (Proof shortened by SN, 23-Feb-2025)

	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		eqcom	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{1}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
5	1 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in B$$
6	5	ne0d	$$⊢R\in \mathrm{Ring}\to B\ne \varnothing$$
7	5	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \underset{\dot{}}{0}\in B$$
8	1 3 2	ring1eq0	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\wedge \underset{\dot{}}{0}\in B\right)\to \left(\underset{\dot{}}{1}=\underset{\dot{}}{0}\to x=\underset{\dot{}}{0}\right)$$
9	7 8	mpd3an3	$$⊢\left(R\in \mathrm{Ring}\wedge x\in B\right)\to \left(\underset{\dot{}}{1}=\underset{\dot{}}{0}\to x=\underset{\dot{}}{0}\right)$$
10	9	impancom	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to \left(x\in B\to x=\underset{\dot{}}{0}\right)$$
11	10	ralrimiv	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to \forall x\in Bx=\underset{\dot{}}{0}$$
12		eqsn	$$⊢B\ne \varnothing \to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall x\in Bx=\underset{\dot{}}{0}\right)$$
13	12	biimpar	$$⊢\left(B\ne \varnothing \wedge \forall x\in Bx=\underset{\dot{}}{0}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
14	6 11 13	syl2an2r	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
15	4 14	sylan2b	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$