Theorem rngosn4

Description: Obsolete as of 25-Jan-2020. Use rngen1zr instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by Mario Carneiro, 30-Apr-2015) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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