Metamath Proof Explorer

Theorem islnr2

Description: Property of being a left-Noetherian ring in terms of finite generation of ideals (the usual "pure ring theory" definition). (Contributed by Stefan O'Rear, 24-Jan-2015)

		Ref	Expression
	Hypotheses	islnr2.b	$⊢ B = {Base}_{R}$
		islnr2.u	$⊢ U = LIdeal (R)$
		islnr2.n	$⊢ N = RSpan (R)$
	Assertion	islnr2	$⊢ R \in LNoeR \leftrightarrow (R \in Ring \land \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$

Proof

Step	Hyp	Ref	Expression
1		islnr2.b	$⊢ B = {Base}_{R}$
2		islnr2.u	$⊢ U = LIdeal (R)$
3		islnr2.n	$⊢ N = RSpan (R)$
4		islnr	$⊢ R \in LNoeR \leftrightarrow (R \in Ring \land ringLMod (R) \in LNoeM)$
5		rlmlmod	$⊢ R \in Ring \to ringLMod (R) \in LMod$
6		rlmbas	$⊢ {Base}_{R} = {Base}_{ringLMod (R)}$
7	1 6	eqtri	$⊢ B = {Base}_{ringLMod (R)}$
8		lidlval	$⊢ LIdeal (R) = LSubSp (ringLMod (R))$
9	2 8	eqtri	$⊢ U = LSubSp (ringLMod (R))$
10		rspval	$⊢ RSpan (R) = LSpan (ringLMod (R))$
11	3 10	eqtri	$⊢ N = LSpan (ringLMod (R))$
12	7 9 11	islnm2	$⊢ ringLMod (R) \in LNoeM \leftrightarrow (ringLMod (R) \in LMod \land \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$
13	12	baib	$⊢ ringLMod (R) \in LMod \to (ringLMod (R) \in LNoeM \leftrightarrow \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$
14	5 13	syl	$⊢ R \in Ring \to (ringLMod (R) \in LNoeM \leftrightarrow \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$
15	14	pm5.32i	$⊢ (R \in Ring \land ringLMod (R) \in LNoeM) \leftrightarrow (R \in Ring \land \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$
16	4 15	bitri	$⊢ R \in LNoeR \leftrightarrow (R \in Ring \land \forall i \in U \exists g \in (𝒫 B \cap Fin) i = N (g))$