Metamath Proof Explorer


Theorem 0ring1eq0

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

Ref Expression
Hypotheses 0ringdif.b
|- B = ( Base ` R )
0ringdif.0
|- .0. = ( 0g ` R )
0ring1eq0.1
|- .1. = ( 1r ` R )
Assertion 0ring1eq0
|- ( R e. ( Ring \ NzRing ) -> .1. = .0. )

Proof

Step Hyp Ref Expression
1 0ringdif.b
 |-  B = ( Base ` R )
2 0ringdif.0
 |-  .0. = ( 0g ` R )
3 0ring1eq0.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. )