Metamath Proof Explorer

Theorem 0ring01eqbi2

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

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 0ring01eqbi2 
|- ( R e. Ring -> ( B = { .0. } <-> .1. = .0. ) )

Proof

Step Hyp Ref Expression
1 0ring.b 
 |-  B = ( Base ` R )
2 0ring.0 
 |-  .0. = ( 0g ` R )
3 0ring01eq.1 
 |-  .1. = ( 1r ` R )
4 fveq2 
 |-  ( B = { .0. } -> ( # ` B ) = ( # ` { .0. } ) )
5 2 fvexi 
 |-  .0. e. _V
6 hashsng 
 |-  ( .0. e. _V -> ( # ` { .0. } ) = 1 )
7 5 6 ax-mp 
 |-  ( # ` { .0. } ) = 1
8 4 7 eqtrdi 
 |-  ( B = { .0. } -> ( # ` B ) = 1 )
9 1 2 3 0ring01eq 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )
10 8 9 sylan2 
 |-  ( ( R e. Ring /\ B = { .0. } ) -> .0. = .1. )
11 10 eqcomd 
 |-  ( ( R e. Ring /\ B = { .0. } ) -> .1. = .0. )
12 11 ex 
 |-  ( R e. Ring -> ( B = { .0. } -> .1. = .0. ) )
13 eqcom 
 |-  ( .1. = .0. <-> .0. = .1. )
14 1 2 3 01eq0ring 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )
15 14 ex 
 |-  ( R e. Ring -> ( .0. = .1. -> B = { .0. } ) )
16 13 15 biimtrid 
 |-  ( R e. Ring -> ( .1. = .0. -> B = { .0. } ) )
17 12 16 impbid 
 |-  ( R e. Ring -> ( B = { .0. } <-> .1. = .0. ) )