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

Metamath Proof Explorer

Theorem 0ring01eq

Description: In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019)

Ref Expression
Hypotheses 0ring.b 
|- B = ( Base ` R )
0ring.0 
|- .0. = ( 0g ` R )
0ring01eq.1 
|- .1. = ( 1r ` R )
Assertion 0ring01eq 
|- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )

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 2 0ring 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
5 1 3 ringidcl 
 |-  ( R e. Ring -> .1. e. B )
6 eleq2 
 |-  ( B = { .0. } -> ( .1. e. B <-> .1. e. { .0. } ) )
7 elsni 
 |-  ( .1. e. { .0. } -> .1. = .0. )
8 7 eqcomd 
 |-  ( .1. e. { .0. } -> .0. = .1. )
9 6 8 biimtrdi 
 |-  ( B = { .0. } -> ( .1. e. B -> .0. = .1. ) )
10 5 9 syl5com 
 |-  ( R e. Ring -> ( B = { .0. } -> .0. = .1. ) )
11 10 adantr 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ( B = { .0. } -> .0. = .1. ) )
12 4 11 mpd 
 |-  ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )