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

Metamath Proof Explorer

Theorem mxidlnzrb

Description: A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024)

Ref Expression
Assertion mxidlnzrb ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 krull ⊢ ( 𝑅 ∈ NzRing → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
2 1 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑅 ∈ NzRing ) → ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
3 19.42v ⊢ ( ∃ 𝑚 ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) ↔ ( 𝑅 ∈ Ring ∧ ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 4 mxidlnzr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
6 5 exlimiv ⊢ ( ∃ 𝑚 ( 𝑅 ∈ Ring ∧ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
7 3 6 sylbir ⊢ ( ( 𝑅 ∈ Ring ∧ ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑅 ∈ NzRing )
8 2 7 impbida ⊢ ( 𝑅 ∈ Ring → ( 𝑅 ∈ NzRing ↔ ∃ 𝑚 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ) )