Theorem 0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-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	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$

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 2	0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
5	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
6		eleq2	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left(\underset{\dot{}}{1}\in B\leftrightarrow \underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\right)$$
7		elsni	$$⊢\underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
8	7	eqcomd	$$⊢\underset{\dot{}}{1}\in \left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
9	6 8	syl6bi	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left(\underset{\dot{}}{1}\in B\to \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
10	5 9	syl5com	$$⊢R\in \mathrm{Ring}\to \left(B=\left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
11	10	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \left(B=\left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)$$
12	4 11	mpd	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$