Metamath Proof Explorer

Theorem lnrfrlm

Description: Finite-dimensional free modules over a Noetherian ring are Noetherian. (Contributed by Stefan O'Rear, 3-Feb-2015)

Ref Expression
Hypothesis lnrfrlm.y ⊢Y=RfreeLModI
Assertion lnrfrlm ⊢R∈LNoeR∧I∈Fin→Y∈LNoeM

Proof

Step Hyp Ref Expression
1 lnrfrlm.y ⊢Y=RfreeLModI
2 1 frlmpwsfi ⊢R∈LNoeR∧I∈Fin→Y=ringLMod⁡R↑𝑠I
3 lnrlnm ⊢R∈LNoeR→ringLMod⁡R∈LNoeM
4 eqid ⊢ringLMod⁡R↑𝑠I=ringLMod⁡R↑𝑠I
5 4 pwslnm ⊢ringLMod⁡R∈LNoeM∧I∈Fin→ringLMod⁡R↑𝑠I∈LNoeM
6 3 5 sylan ⊢R∈LNoeR∧I∈Fin→ringLMod⁡R↑𝑠I∈LNoeM
7 2 6 eqeltrd ⊢R∈LNoeR∧I∈Fin→Y∈LNoeM