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	$⊢ B = {Base}_{R}$
	Assertion	mxidlnzr	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to R \in NzRing$

Step	Hyp	Ref	Expression
1		mxidlval.1	$⊢ B = {Base}_{R}$
2	1	mxidlidl	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to M \in LIdeal (R)$
3		eqid	$⊢ LIdeal (R) = LIdeal (R)$
4		eqid	$⊢ 0_{R} = 0_{R}$
5	3 4	lidl0cl	$⊢ (R \in Ring \land M \in LIdeal (R)) \to 0_{R} \in M$
6	2 5	syldan	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to 0_{R} \in M$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	1 7	mxidln1	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to \neg 1_{R} \in M$
9		nelne2	$⊢ (0_{R} \in M \land \neg 1_{R} \in M) \to 0_{R} \neq 1_{R}$
10	6 8 9	syl2anc	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to 0_{R} \neq 1_{R}$
11	10	necomd	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to 1_{R} \neq 0_{R}$
12	7 4	isnzr	$⊢ R \in NzRing \leftrightarrow (R \in Ring \land 1_{R} \neq 0_{R})$
13	12	biimpri	$⊢ (R \in Ring \land 1_{R} \neq 0_{R}) \to R \in NzRing$
14	11 13	syldan	$⊢ (R \in Ring \land M \in MaxIdeal (R)) \to R \in NzRing$

Metamath Proof Explorer