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 ‘ 𝑅 )
	drnglidl1ne0.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	drnglidl1ne0	⊢ ( 𝑅 ∈ NzRing → 𝐵 ≠ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		drnglidl1ne0.1	⊢ 0 = ( 0g ‘ 𝑅 )
2		drnglidl1ne0.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
4		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5	2 4	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
6	3 5	syl	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
7	4 1	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
8		nelsn	⊢ ( ( 1r ‘ 𝑅 ) ≠ 0 → ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } )
9	7 8	syl	⊢ ( 𝑅 ∈ NzRing → ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } )
10		nelne1	⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ¬ ( 1r ‘ 𝑅 ) ∈ { 0 } ) → 𝐵 ≠ { 0 } )
11	6 9 10	syl2anc	⊢ ( 𝑅 ∈ NzRing → 𝐵 ≠ { 0 } )