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 )