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

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 )