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 ‘ 𝑅 )
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 } )