This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( 𝑍 = 𝑈 ↔ 𝑋 = { 𝑍 } ) )