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	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	0ring.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	0ring.3	⊢ 𝑋 = ran 𝐺
	0ring.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
	0ring.5	⊢ 𝑈 = ( GId ‘ 𝐻 )
Assertion	0rngo	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 = 𝑈 ↔ 𝑋 = { 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		0ring.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		0ring.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		0ring.3	⊢ 𝑋 = ran 𝐺
4		0ring.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5		0ring.5	⊢ 𝑈 = ( GId ‘ 𝐻 )
6	4	fvexi	⊢ 𝑍 ∈ V
7	6	snid	⊢ 𝑍 ∈ { 𝑍 }
8		eleq1	⊢ ( 𝑍 = 𝑈 → ( 𝑍 ∈ { 𝑍 } ↔ 𝑈 ∈ { 𝑍 } ) )
9	7 8	mpbii	⊢ ( 𝑍 = 𝑈 → 𝑈 ∈ { 𝑍 } )
10	1 4	0idl	⊢ ( 𝑅 ∈ RingOps → { 𝑍 } ∈ ( Idl ‘ 𝑅 ) )
11	1 2 3 5	1idl	⊢ ( ( 𝑅 ∈ RingOps ∧ { 𝑍 } ∈ ( Idl ‘ 𝑅 ) ) → ( 𝑈 ∈ { 𝑍 } ↔ { 𝑍 } = 𝑋 ) )
12	10 11	mpdan	⊢ ( 𝑅 ∈ RingOps → ( 𝑈 ∈ { 𝑍 } ↔ { 𝑍 } = 𝑋 ) )
13	9 12	imbitrid	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 = 𝑈 → { 𝑍 } = 𝑋 ) )
14		eqcom	⊢ ( { 𝑍 } = 𝑋 ↔ 𝑋 = { 𝑍 } )
15	13 14	imbitrdi	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 = 𝑈 → 𝑋 = { 𝑍 } ) )
16	1	rneqi	⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
17	3 16	eqtri	⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
18	17 2 5	rngo1cl	⊢ ( 𝑅 ∈ RingOps → 𝑈 ∈ 𝑋 )
19		eleq2	⊢ ( 𝑋 = { 𝑍 } → ( 𝑈 ∈ 𝑋 ↔ 𝑈 ∈ { 𝑍 } ) )
20		elsni	⊢ ( 𝑈 ∈ { 𝑍 } → 𝑈 = 𝑍 )
21	20	eqcomd	⊢ ( 𝑈 ∈ { 𝑍 } → 𝑍 = 𝑈 )
22	19 21	biimtrdi	⊢ ( 𝑋 = { 𝑍 } → ( 𝑈 ∈ 𝑋 → 𝑍 = 𝑈 ) )
23	18 22	syl5com	⊢ ( 𝑅 ∈ RingOps → ( 𝑋 = { 𝑍 } → 𝑍 = 𝑈 ) )
24	15 23	impbid	⊢ ( 𝑅 ∈ RingOps → ( 𝑍 = 𝑈 ↔ 𝑋 = { 𝑍 } ) )