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. } )