Theorem rngosn6

Description: Obsolete as of 25-Jan-2020. Use ringen1zr or srgen1zr instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010) (New usage is discouraged.)

	Ref	Expression
Hypotheses	on1el3.1	$$⊢G=1^{st}\left(R\right)$$
	on1el3.2	$$⊢X=\mathrm{ran}G$$
	on1el3.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
Assertion	rngosn6	$$⊢R\in \mathrm{RingOps}\to \left(X\approx 1_{𝑜}\leftrightarrow R=⟨\left\{⟨⟨Z,Z⟩,Z⟩\right\},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right)$$

Proof

Step	Hyp	Ref	Expression
1		on1el3.1	$$⊢G=1^{st}\left(R\right)$$
2		on1el3.2	$$⊢X=\mathrm{ran}G$$
3		on1el3.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
4	1 2 3	rngo0cl	$$⊢R\in \mathrm{RingOps}\to Z\in X$$
5	1 2	rngosn4	$$⊢\left(R\in \mathrm{RingOps}\wedge Z\in X\right)\to \left(X\approx 1_{𝑜}\leftrightarrow R=⟨\left\{⟨⟨Z,Z⟩,Z⟩\right\},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right)$$
6	4 5	mpdan	$$⊢R\in \mathrm{RingOps}\to \left(X\approx 1_{𝑜}\leftrightarrow R=⟨\left\{⟨⟨Z,Z⟩,Z⟩\right\},\left\{⟨⟨Z,Z⟩,Z⟩\right\}⟩\right)$$