Metamath Proof Explorer


Theorem mxidlnzr

Description: A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
Assertion mxidlnzr ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )

Proof

Step Hyp Ref Expression
1 mxidlval.1 𝐵 = ( Base ‘ 𝑅 )
2 1 mxidlidl ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
3 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4 eqid ( 0g𝑅 ) = ( 0g𝑅 )
5 3 4 lidl0cl ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g𝑅 ) ∈ 𝑀 )
6 2 5 syldan ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 0g𝑅 ) ∈ 𝑀 )
7 eqid ( 1r𝑅 ) = ( 1r𝑅 )
8 1 7 mxidln1 ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ¬ ( 1r𝑅 ) ∈ 𝑀 )
9 nelne2 ( ( ( 0g𝑅 ) ∈ 𝑀 ∧ ¬ ( 1r𝑅 ) ∈ 𝑀 ) → ( 0g𝑅 ) ≠ ( 1r𝑅 ) )
10 6 8 9 syl2anc ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 0g𝑅 ) ≠ ( 1r𝑅 ) )
11 10 necomd ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → ( 1r𝑅 ) ≠ ( 0g𝑅 ) )
12 7 4 isnzr ( 𝑅 ∈ NzRing ↔ ( 𝑅 ∈ Ring ∧ ( 1r𝑅 ) ≠ ( 0g𝑅 ) ) )
13 12 biimpri ( ( 𝑅 ∈ Ring ∧ ( 1r𝑅 ) ≠ ( 0g𝑅 ) ) → 𝑅 ∈ NzRing )
14 11 13 syldan ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )