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

Metamath Proof Explorer

Theorem 0ring01eqbi

Description: In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010) (Revised by AV, 23-Jan-2020)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 0ring01eqbi 
|- ( R e. Ring -> ( B ~~ 1o <-> .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 1 fvexi 
 |-  B e. _V
5 hashen1 
 |-  ( B e. _V -> ( ( # ` B ) = 1 <-> B ~~ 1o ) )
6 4 5 mp1i 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 <-> B ~~ 1o ) )
7 1 2 3 0ring01eq 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )
8 7 eqcomd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .1. = .0. )
9 8 ex 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 -> .1. = .0. ) )
10 eqcom 
 |-  ( .1. = .0. <-> .0. = .1. )
11 1 2 3 01eq0ring 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )
12 fveq2 
 |-  ( B = { .0. } -> ( # ` B ) = ( # ` { .0. } ) )
13 2 fvexi 
 |-  .0. e. _V
14 hashsng 
 |-  ( .0. e. _V -> ( # ` { .0. } ) = 1 )
15 13 14 mp1i 
 |-  ( B = { .0. } -> ( # ` { .0. } ) = 1 )
16 12 15 eqtrd 
 |-  ( B = { .0. } -> ( # ` B ) = 1 )
17 11 16 syl 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> ( # ` B ) = 1 )
18 17 ex 
 |-  ( R e. Ring -> ( .0. = .1. -> ( # ` B ) = 1 ) )
19 10 18 biimtrid 
 |-  ( R e. Ring -> ( .1. = .0. -> ( # ` B ) = 1 ) )
20 9 19 impbid 
 |-  ( R e. Ring -> ( ( # ` B ) = 1 <-> .1. = .0. ) )
21 6 20 bitr3d 
 |-  ( R e. Ring -> ( B ~~ 1o <-> .1. = .0. ) )