Theorem lnrlnm

Description: Left-Noetherian rings have Noetherian associated modules. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Assertion	lnrlnm	⊢ ( 𝐴 ∈ LNoeR → ( ringLMod ‘ 𝐴 ) ∈ LNoeM )

Proof

Step	Hyp	Ref	Expression
1		islnr	⊢ ( 𝐴 ∈ LNoeR ↔ ( 𝐴 ∈ Ring ∧ ( ringLMod ‘ 𝐴 ) ∈ LNoeM ) )
2	1	simprbi	⊢ ( 𝐴 ∈ LNoeR → ( ringLMod ‘ 𝐴 ) ∈ LNoeM )