Theorem ringen1zr0

Description: The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 , and semirings, see srgen1zr0 . (Contributed by FL, 15-Feb-2010) (Revised by AV, 25-Jan-2020) (Proof shortened by AV, 19-Jun-2026)

	Ref	Expression
Hypotheses	ring1zr.b	$$⊢B={\mathrm{Base}}_R$$
	ring1zr.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	ring1zr.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
	ringen1zr0.0	$$⊢Z=0_R$$
Assertion	ringen1zr0	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\wedge \underset{\dot{}}{\ast }Fn\left(B\times B\right)\right)\to \left(B\approx 1_{𝑜}\leftrightarrow \left(\underset{\dot{}}{+}=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ring1zr.b	$$⊢B={\mathrm{Base}}_R$$
2		ring1zr.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		ring1zr.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
4		ringen1zr0.0	$$⊢Z=0_R$$
5		ringrng	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Rng}$$
6	1 2 3 4	rngen1zr0	$$⊢\left(R\in \mathrm{Rng}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\wedge \underset{\dot{}}{\ast }Fn\left(B\times B\right)\right)\to \left(B\approx 1_{𝑜}\leftrightarrow \left(\underset{\dot{}}{+}=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\right)\right)$$
7	5 6	syl3an1	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{+}Fn\left(B\times B\right)\wedge \underset{\dot{}}{\ast }Fn\left(B\times B\right)\right)\to \left(B\approx 1_{𝑜}\leftrightarrow \left(\underset{\dot{}}{+}=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨Z,Z⟩,Z⟩\right\}\right)\right)$$