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

Metamath Proof Explorer

Theorem drnglidl1ne0

Description: In a nonzero ring, the zero ideal is different of the unit ideal. (Contributed by Thierry Arnoux, 16-Mar-2025)

Ref Expression
Hypotheses drnglidl1ne0.1 
|- .0. = ( 0g ` R )
drnglidl1ne0.2 
|- B = ( Base ` R )
Assertion drnglidl1ne0 
|- ( R e. NzRing -> B =/= { .0. } )

Proof

Step Hyp Ref Expression
1 drnglidl1ne0.1 
 |-  .0. = ( 0g ` R )
2 drnglidl1ne0.2 
 |-  B = ( Base ` R )
3 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
4 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
5 2 4 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. B )
6 3 5 syl 
 |-  ( R e. NzRing -> ( 1r ` R ) e. B )
7 4 1 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
8 nelsn 
 |-  ( ( 1r ` R ) =/= .0. -> -. ( 1r ` R ) e. { .0. } )
9 7 8 syl 
 |-  ( R e. NzRing -> -. ( 1r ` R ) e. { .0. } )
10 nelne1 
 |-  ( ( ( 1r ` R ) e. B /\ -. ( 1r ` R ) e. { .0. } ) -> B =/= { .0. } )
11 6 9 10 syl2anc 
 |-  ( R e. NzRing -> B =/= { .0. } )