Theorem rngen1zr0

Description: The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010) (Revised by AV, 18-Jun-2026)

	Ref	Expression
Hypotheses	rng1zr.b	$$⊢B={\mathrm{Base}}_R$$
	rng1zr.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	rng1zr.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
	rngen1zr0.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	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\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rng1zr.b	$$⊢B={\mathrm{Base}}_R$$
2		rng1zr.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		rng1zr.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_R$$
4		rngen1zr0.0	$$⊢\underset{\dot{}}{0}=0_R$$
5	1 4	rng0cl	$$⊢R\in \mathrm{Rng}\to \underset{\dot{}}{0}\in B$$
6	5	3ad2ant1	$$⊢\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 \underset{\dot{}}{0}\in B$$
7	1 2 3	rngen1zr	$$⊢\left(\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)\wedge \underset{\dot{}}{0}\in B\right)\to \left(B\approx 1_{𝑜}\leftrightarrow \left(\underset{\dot{}}{+}=\left\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\right)\right)$$
8	6 7	mpdan	$$⊢\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\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\wedge \underset{\dot{}}{\ast }=\left\{⟨⟨\underset{\dot{}}{0},\underset{\dot{}}{0}⟩,\underset{\dot{}}{0}⟩\right\}\right)\right)$$