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	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow \exists m m \in MaxIdeal (R))$

Step	Hyp	Ref	Expression
1		krull	$⊢ R \in NzRing \to \exists m m \in MaxIdeal (R)$
2	1	adantl	$⊢ (R \in Ring \land R \in NzRing) \to \exists m m \in MaxIdeal (R)$
3		19.42v	$⊢ \exists m (R \in Ring \land m \in MaxIdeal (R)) \leftrightarrow (R \in Ring \land \exists m m \in MaxIdeal (R))$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5	4	mxidlnzr	$⊢ (R \in Ring \land m \in MaxIdeal (R)) \to R \in NzRing$
6	5	exlimiv	$⊢ \exists m (R \in Ring \land m \in MaxIdeal (R)) \to R \in NzRing$
7	3 6	sylbir	$⊢ (R \in Ring \land \exists m m \in MaxIdeal (R)) \to R \in NzRing$
8	2 7	impbida	$⊢ R \in Ring \to (R \in NzRing \leftrightarrow \exists m m \in MaxIdeal (R))$

Metamath Proof Explorer