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