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

Metamath Proof Explorer

Theorem 01eq0ring

Description: If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019) (Proof shortened by SN, 23-Feb-2025)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 01eq0ring 
|- ( ( R e. Ring /\ .0. = .1. ) -> B = { .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 eqcom 
 |-  ( .0. = .1. <-> .1. = .0. )
5 1 2 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
6 5 ne0d 
 |-  ( R e. Ring -> B =/= (/) )
7 5 adantr 
 |-  ( ( R e. Ring /\ x e. B ) -> .0. e. B )
8 1 3 2 ring1eq0 
 |-  ( ( R e. Ring /\ x e. B /\ .0. e. B ) -> ( .1. = .0. -> x = .0. ) )
9 7 8 mpd3an3 
 |-  ( ( R e. Ring /\ x e. B ) -> ( .1. = .0. -> x = .0. ) )
10 9 impancom 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> ( x e. B -> x = .0. ) )
11 10 ralrimiv 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> A. x e. B x = .0. )
12 eqsn 
 |-  ( B =/= (/) -> ( B = { .0. } <-> A. x e. B x = .0. ) )
13 12 biimpar 
 |-  ( ( B =/= (/) /\ A. x e. B x = .0. ) -> B = { .0. } )
14 6 11 13 syl2an2r 
 |-  ( ( R e. Ring /\ .1. = .0. ) -> B = { .0. } )
15 4 14 sylan2b 
 |-  ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )