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 
|- G = ( 1st ` R )
0ring.2 
|- H = ( 2nd ` R )
0ring.3 
|- X = ran G
0ring.4 
|- Z = ( GId ` G )
0ring.5 
|- U = ( GId ` H )
Assertion 0rngo 
|- ( R e. RingOps -> ( Z = U <-> X = { Z } ) )

Proof

Step Hyp Ref Expression
1 0ring.1 
 |-  G = ( 1st ` R )
2 0ring.2 
 |-  H = ( 2nd ` R )
3 0ring.3 
 |-  X = ran G
4 0ring.4 
 |-  Z = ( GId ` G )
5 0ring.5 
 |-  U = ( GId ` H )
6 4 fvexi 
 |-  Z e. _V
7 6 snid 
 |-  Z e. { Z }
8 eleq1 
 |-  ( Z = U -> ( Z e. { Z } <-> U e. { Z } ) )
9 7 8 mpbii 
 |-  ( Z = U -> U e. { Z } )
10 1 4 0idl 
 |-  ( R e. RingOps -> { Z } e. ( Idl ` R ) )
11 1 2 3 5 1idl 
 |-  ( ( R e. RingOps /\ { Z } e. ( Idl ` R ) ) -> ( U e. { Z } <-> { Z } = X ) )
12 10 11 mpdan 
 |-  ( R e. RingOps -> ( U e. { Z } <-> { Z } = X ) )
13 9 12 imbitrid 
 |-  ( R e. RingOps -> ( Z = U -> { Z } = X ) )
14 eqcom 
 |-  ( { Z } = X <-> X = { Z } )
15 13 14 imbitrdi 
 |-  ( R e. RingOps -> ( Z = U -> X = { Z } ) )
16 1 rneqi 
 |-  ran G = ran ( 1st ` R )
17 3 16 eqtri 
 |-  X = ran ( 1st ` R )
18 17 2 5 rngo1cl 
 |-  ( R e. RingOps -> U e. X )
19 eleq2 
 |-  ( X = { Z } -> ( U e. X <-> U e. { Z } ) )
20 elsni 
 |-  ( U e. { Z } -> U = Z )
21 20 eqcomd 
 |-  ( U e. { Z } -> Z = U )
22 19 21 biimtrdi 
 |-  ( X = { Z } -> ( U e. X -> Z = U ) )
23 18 22 syl5com 
 |-  ( R e. RingOps -> ( X = { Z } -> Z = U ) )
24 15 23 impbid 
 |-  ( R e. RingOps -> ( Z = U <-> X = { Z } ) )