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

Metamath Proof Explorer

Theorem 0ring1eq0

Description: In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 0ring1eq0 
|- ( R e. ( Ring \ NzRing ) -> .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 eldif 
 |-  ( R e. ( Ring \ NzRing ) <-> ( R e. Ring /\ -. R e. NzRing ) )
5 0ringnnzr 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 6 2 3 0ring01eq 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .0. = .1. )
8 7 eqcomd 
 |-  ( ( R e. Ring /\ ( # ` ( Base ` R ) ) = 1 ) -> .1. = .0. )
9 8 ex 
 |-  ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 -> .1. = .0. ) )
10 5 9 sylbird 
 |-  ( R e. Ring -> ( -. R e. NzRing -> .1. = .0. ) )
11 10 imp 
 |-  ( ( R e. Ring /\ -. R e. NzRing ) -> .1. = .0. )
12 4 11 sylbi 
 |-  ( R e. ( Ring \ NzRing ) -> .1. = .0. )