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

Metamath Proof Explorer

Theorem ringelnzr

Description: A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015) (Revised by Mario Carneiro, 13-Jun-2015)

Ref Expression
Hypotheses ringelnzr.z 
|- .0. = ( 0g ` R )
ringelnzr.b 
|- B = ( Base ` R )
Assertion ringelnzr 
|- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )

Proof

Step Hyp Ref Expression
1 ringelnzr.z 
 |-  .0. = ( 0g ` R )
2 ringelnzr.b 
 |-  B = ( Base ` R )
3 simpl 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. Ring )
4 eldifsni 
 |-  ( X e. ( B \ { .0. } ) -> X =/= .0. )
5 4 adantl 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X =/= .0. )
6 eldifi 
 |-  ( X e. ( B \ { .0. } ) -> X e. B )
7 6 adantl 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> X e. B )
8 2 1 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
9 8 adantr 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> .0. e. B )
10 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
11 2 10 1 ring1eq0 
 |-  ( ( R e. Ring /\ X e. B /\ .0. e. B ) -> ( ( 1r ` R ) = .0. -> X = .0. ) )
12 3 7 9 11 syl3anc 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( ( 1r ` R ) = .0. -> X = .0. ) )
13 12 necon3d 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( X =/= .0. -> ( 1r ` R ) =/= .0. ) )
14 5 13 mpd 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> ( 1r ` R ) =/= .0. )
15 10 1 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= .0. ) )
16 3 14 15 sylanbrc 
 |-  ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )