Theorem 0rngo

Description: In a ring, 0 = 1 iff the ring contains only 0 . (Contributed by Jeff Madsen, 6-Jan-2011)

	Ref	Expression
Hypotheses	0ring.1	$$⊢G=1^{st}\left(R\right)$$
	0ring.2	$$⊢H=2^{nd}\left(R\right)$$
	0ring.3	$$⊢X=\mathrm{ran}G$$
	0ring.4	$$⊢Z=\mathrm{GId}\left(G\right)$$
	0ring.5	$$⊢U=\mathrm{GId}\left(H\right)$$
Assertion	0rngo	$$⊢R\in \mathrm{RingOps}\to \left(Z=U\leftrightarrow X=\left\{Z\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ring.1	$$⊢G=1^{st}\left(R\right)$$
2		0ring.2	$$⊢H=2^{nd}\left(R\right)$$
3		0ring.3	$$⊢X=\mathrm{ran}G$$
4		0ring.4	$$⊢Z=\mathrm{GId}\left(G\right)$$
5		0ring.5	$$⊢U=\mathrm{GId}\left(H\right)$$
6	4	fvexi	$$⊢Z\in \mathrm{V}$$
7	6	snid	$$⊢Z\in \left\{Z\right\}$$
8		eleq1	$$⊢Z=U\to \left(Z\in \left\{Z\right\}\leftrightarrow U\in \left\{Z\right\}\right)$$
9	7 8	mpbii	$$⊢Z=U\to U\in \left\{Z\right\}$$
10	1 4	0idl	$$⊢R\in \mathrm{RingOps}\to \left\{Z\right\}\in \mathrm{Idl}\left(R\right)$$
11	1 2 3 5	1idl	$$⊢\left(R\in \mathrm{RingOps}\wedge \left\{Z\right\}\in \mathrm{Idl}\left(R\right)\right)\to \left(U\in \left\{Z\right\}\leftrightarrow \left\{Z\right\}=X\right)$$
12	10 11	mpdan	$$⊢R\in \mathrm{RingOps}\to \left(U\in \left\{Z\right\}\leftrightarrow \left\{Z\right\}=X\right)$$
13	9 12	imbitrid	$$⊢R\in \mathrm{RingOps}\to \left(Z=U\to \left\{Z\right\}=X\right)$$
14		eqcom	$$⊢\left\{Z\right\}=X\leftrightarrow X=\left\{Z\right\}$$
15	13 14	imbitrdi	$$⊢R\in \mathrm{RingOps}\to \left(Z=U\to X=\left\{Z\right\}\right)$$
16	1	rneqi	$$⊢\mathrm{ran}G=\mathrm{ran}{1}^{st}\left(R\right)$$
17	3 16	eqtri	$$⊢X=\mathrm{ran}{1}^{st}\left(R\right)$$
18	17 2 5	rngo1cl	$$⊢R\in \mathrm{RingOps}\to U\in X$$
19		eleq2	$$⊢X=\left\{Z\right\}\to \left(U\in X\leftrightarrow U\in \left\{Z\right\}\right)$$
20		elsni	$$⊢U\in \left\{Z\right\}\to U=Z$$
21	20	eqcomd	$$⊢U\in \left\{Z\right\}\to Z=U$$
22	19 21	syl6bi	$$⊢X=\left\{Z\right\}\to \left(U\in X\to Z=U\right)$$
23	18 22	syl5com	$$⊢R\in \mathrm{RingOps}\to \left(X=\left\{Z\right\}\to Z=U\right)$$
24	15 23	impbid	$$⊢R\in \mathrm{RingOps}\to \left(Z=U\leftrightarrow X=\left\{Z\right\}\right)$$