Metamath Proof Explorer

Theorem lnrlnm

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

Ref Expression
Assertion lnrlnm 
|- ( A e. LNoeR -> ( ringLMod ` A ) e. LNoeM )

Proof

Step Hyp Ref Expression
1 islnr 
 |-  ( A e. LNoeR <-> ( A e. Ring /\ ( ringLMod ` A ) e. LNoeM ) )
2 1 simprbi 
 |-  ( A e. LNoeR -> ( ringLMod ` A ) e. LNoeM )