Theorem islnr

Description: Property of a left-Noetherian ring. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	islnr	$$⊢A\in \mathrm{LNoeR}\leftrightarrow \left(A\in \mathrm{Ring}\wedge \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢a=A\to \mathrm{ringLMod}\left(a\right)=\mathrm{ringLMod}\left(A\right)$$
2	1	eleq1d	$$⊢a=A\to \left(\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}\leftrightarrow \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}\right)$$
3		df-lnr	$$⊢\mathrm{LNoeR}=\left\{a\in \mathrm{Ring}|\mathrm{ringLMod}\left(a\right)\in \mathrm{LNoeM}\right\}$$
4	2 3	elrab2	$$⊢A\in \mathrm{LNoeR}\leftrightarrow \left(A\in \mathrm{Ring}\wedge \mathrm{ringLMod}\left(A\right)\in \mathrm{LNoeM}\right)$$